section ‹Auxiliary lemmas›

theory AuxLemmas imports Main begin

text ‹Lemma concerning maps and ‹@››

lemma map_append_append_maps:
  assumes map:"map f xs = ys@zs"
  obtains xs' xs'' where "map f xs' = ys" and "map f xs'' = zs" and "xs=xs'@xs''"
by (metis append_eq_conv_conj append_take_drop_id assms drop_map take_map that)


text ‹Lemma concerning splitting of @{term list}s›

lemma  path_split_general:
assumes all:"∀zs. xs ≠ ys@zs"
obtains j zs where "xs = (take j ys)@zs" and "j < length ys"
  and "∀k > j. ∀zs'. xs ≠ (take k ys)@zs'"
proof(atomize_elim)
  from ‹∀zs. xs ≠ ys@zs›
  show "∃j zs. xs = take j ys @ zs ∧ j < length ys ∧ 
               (∀k>j. ∀zs'. xs ≠ take k ys @ zs')"
  proof(induct ys arbitrary:xs)
    case Nil thus ?case by auto
  next
    case (Cons y' ys')
    note IH = ‹⋀xs. ∀zs. xs ≠ ys' @ zs ⟹
      ∃j zs. xs = take j ys' @ zs ∧ j < length ys' ∧ 
      (∀k. j < k ⟶ (∀zs'. xs ≠ take k ys' @ zs'))›
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with ‹∀zs. xs ≠ (y' # ys') @ zs› have "x' ≠ y' ∨ (∀zs. xs' ≠ ys' @ zs)"
        by simp
      show ?thesis
      proof(cases "x' = y'")
        case True
        with ‹x' ≠ y' ∨ (∀zs. xs' ≠ ys' @ zs)› have "∀zs. xs' ≠ ys' @ zs" by simp
        from IH[OF this] have "∃j zs. xs' = take j ys' @ zs ∧ j < length ys' ∧
          (∀k. j < k ⟶ (∀zs'. xs' ≠ take k ys' @ zs'))" .
        then obtain j zs where "xs' = take j ys' @ zs"
          and "j < length ys'"
          and all_sub:"∀k. j < k ⟶ (∀zs'. xs' ≠ take k ys' @ zs')"
          by blast
        from ‹xs' = take j ys' @ zs› True
          have "(x'#xs') = take (Suc j) (y' # ys') @ zs"
          by simp
        from all_sub True have all_imp:"∀k. j < k ⟶ 
          (∀zs'. (x'#xs') ≠ take (Suc k) (y' # ys') @ zs')"
          by auto
        { fix l assume "(Suc j) < l"
          then obtain k where [simp]:"l = Suc k" by(cases l) auto
          with ‹(Suc j) < l› have "j < k" by simp
          with all_imp 
          have "∀zs'. (x'#xs') ≠ take (Suc k) (y' # ys') @ zs'"
            by simp
          hence "∀zs'. (x'#xs') ≠ take l (y' # ys') @ zs'"
            by simp }
        with ‹(x'#xs') = take (Suc j) (y' # ys') @ zs› ‹j < length ys'› Cons
        show ?thesis by (metis Suc_length_conv less_Suc_eq_0_disj)
      next
        case False
        with Cons have "∀i zs'. i > 0 ⟶ xs ≠ take i (y' # ys') @ zs'"
          by auto(case_tac i,auto)
        moreover
        have "∃zs. xs = take 0 (y' # ys') @ zs" by simp
        ultimately show ?thesis by(rule_tac x="0" in exI,auto)
      qed
    qed
  qed
qed


end

chapter ‹The Framework›

theory BasicDefs imports AuxLemmas begin

text ‹
  As slicing is a program analysis that can be completely based on the
  information given in the CFG, we want to provide a framework which
  allows us to formalize and prove properties of slicing regardless of
  the actual programming language. So the starting point for the formalization 
  is the definition of an abstract CFG, i.e.\ without considering features 
  specific for certain languages. By doing so we ensure that our framework 
  is as generic as possible since all proofs hold for every language whose 
  CFG conforms to this abstract CFG.

  Static Slicing analyses a CFG prior to execution. Whereas dynamic
  slicing can provide better results for certain inputs (i.e.\ trace and
  initial state), static slicing is more conservative but provides
  results independent of inputs. 

  Correctness for static slicing is defined using a weak
  simulation between nodes and states when traversing the original and
  the sliced graph. The weak simulation property demands that if a
  (node,state) tuples $(n_1,s_1)$ simulates $(n_2,s_2)$
  and making an observable move in the original graph leads from 
  $(n_1,s_1)$ to $(n_1',s_1')$, this tuple simulates a 
  tuple $(n_2,s_2)$ which is the result of making an
  observable move in the sliced graph beginning in $(n_2',s_2')$.  
›

section ‹Basic Definitions›

fun fun_upds :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list ⇒ ('a ⇒ 'b)"
where "fun_upds f [] ys = f"
  | "fun_upds f xs [] = f"
  | "fun_upds f (x#xs) (y#ys) = (fun_upds f xs ys)(x := y)"

notation fun_upds ("_'(_ /[:=]/ _')")

lemma fun_upds_nth:
  "⟦i < length xs; length xs = length ys; distinct xs⟧
  ⟹ f(xs [:=] ys)(xs!i) = (ys!i)"
proof(induct xs arbitrary:ys i)
  case Nil thus ?case by simp
next
  case (Cons x' xs')
  note IH = ‹⋀ys i. ⟦i < length xs'; length xs' = length ys; distinct xs'⟧
    ⟹ f(xs' [:=] ys) (xs'!i) = ys!i›
  from ‹distinct (x'#xs')› have "distinct xs'" and "x' ∉ set xs'" by simp_all
  from ‹length (x'#xs') = length ys› obtain y' ys' where [simp]:"ys = y'#ys'"
    and "length xs' = length ys'"
    by(cases ys) auto
  show ?case
  proof(cases i)
    case 0 thus ?thesis by simp
  next
    case (Suc j)
    with ‹i < length (x'#xs')› have "j < length xs'" by simp
    from IH[OF this ‹length xs' = length ys'› ‹distinct xs'›]
    have "f(xs' [:=] ys') (xs'!j) = ys'!j" .
    with ‹x' ∉ set xs'› ‹j < length xs'›
    have "f((x'#xs') [:=] ys) ((x'#xs')!(Suc j)) = ys!(Suc j)" by fastforce
    with Suc show ?thesis by simp
  qed
qed


lemma fun_upds_eq:
  assumes "V ∈ set xs" and "length xs = length ys" and "distinct xs"
  shows "f(xs [:=] ys) V = f'(xs [:=] ys) V"
proof -
  from ‹V ∈ set xs› obtain i where "i < length xs" and "xs!i = V"
    by(fastforce simp:in_set_conv_nth)
  with ‹length xs = length ys› ‹distinct xs›
  have "f(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
  moreover
  from ‹i < length xs› ‹xs!i = V› ‹length xs = length ys› ‹distinct xs›
  have "f'(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
  ultimately show ?thesis using ‹xs!i = V› by simp
qed


lemma fun_upds_notin:"x ∉ set xs ⟹ f(xs [:=] ys) x = f x"
by(induct xs arbitrary:ys,auto,case_tac ys,auto)


subsection ‹‹distinct_fst››
 
definition distinct_fst :: "('a × 'b) list ⇒ bool" where
  "distinct_fst  ≡  distinct ∘ map fst"

lemma distinct_fst_Nil [simp]:
  "distinct_fst []" 
  by(simp add:distinct_fst_def)

lemma distinct_fst_Cons [simp]:
  "distinct_fst ((k,x)#kxs) = (distinct_fst kxs ∧ (∀y. (k,y) ∉ set kxs))"
by(auto simp:distinct_fst_def image_def)


lemma distinct_fst_isin_same_fst:
  "⟦(x,y) ∈ set xs; (x,y') ∈ set xs; distinct_fst xs⟧
  ⟹ y = y'"
by(induct xs,auto simp:distinct_fst_def image_def)


subsection‹Edge kinds›

text ‹Every procedure has a unique name, e.g. in object oriented languages
  ‹pname› refers to class + procedure.›

text ‹A state is a call stack of tuples, which consists of:
  \begin{enumerate}
  \item data information, i.e.\ a mapping from the local variables in the call 
  frame to their values, and
  \item control flow information, e.g.\ which node called the current procedure.
  \end{enumerate}

  Update and predicate edges check and manipulate only the data information
  of the top call stack element. Call and return edges however may use the data and
  control flow information present in the top stack element to state if this edge is
  traversable. The call edge additionally has a list of functions to determine what
  values the parameters have in a certain call frame and control flow information for
  the return. The return edge is concerned with passing the values 
  of the return parameter values to the underlying stack frame. See the funtions 
  ‹transfer› and ‹pred› in locale ‹CFG›.›

datatype (dead 'var, dead 'val, dead 'ret, dead 'pname) edge_kind =
    UpdateEdge "('var ⇀ 'val) ⇒ ('var ⇀ 'val)"                  ("⇑_")
  | PredicateEdge "('var ⇀ 'val) ⇒ bool"                         ("'(_')⇩√")
  | CallEdge "('var ⇀ 'val) × 'ret ⇒ bool" "'ret" "'pname"  
             "(('var ⇀ 'val) ⇀ 'val) list"                       ("_:_↪⇘_⇙_" 70)
  | ReturnEdge "('var ⇀ 'val) × 'ret ⇒ bool" "'pname" 
               "('var ⇀ 'val) ⇒ ('var ⇀ 'val) ⇒ ('var ⇀ 'val)" ("_↩⇘_⇙_" 70)


definition intra_kind :: "('var,'val,'ret,'pname) edge_kind ⇒ bool"
where "intra_kind et ≡ (∃f. et = ⇑f) ∨ (∃Q. et = (Q)⇩√)"


lemma edge_kind_cases [case_names Intra Call Return]:
  "⟦intra_kind et ⟹ P; ⋀Q r p fs. et = Q:r↪⇘p⇙fs ⟹ P;
    ⋀Q p f. et = Q↩⇘p⇙f ⟹ P⟧ ⟹ P"
by(cases et,auto simp:intra_kind_def)


end

section ‹CFG›

theory CFG imports BasicDefs begin

subsection ‹The abstract CFG›

subsubsection ‹Locale fixes and assumptions›

locale CFG =
  fixes sourcenode :: "'edge ⇒ 'node"
  fixes targetnode :: "'edge ⇒ 'node"
  fixes kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind"
  fixes valid_edge :: "'edge ⇒ bool"
  fixes Entry::"'node" ("'('_Entry'_')")
  fixes get_proc::"'node ⇒ 'pname"
  fixes get_return_edges::"'edge ⇒ 'edge set"
  fixes procs::"('pname × 'var list × 'var list) list"
  fixes Main::"'pname"
  assumes Entry_target [dest]: "⟦valid_edge a; targetnode a = (_Entry_)⟧ ⟹ False"
  and get_proc_Entry:"get_proc (_Entry_) = Main"
  and Entry_no_call_source:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; sourcenode a = (_Entry_)⟧ ⟹ False"
  and edge_det: 
    "⟦valid_edge a; valid_edge a'; sourcenode a = sourcenode a'; 
      targetnode a = targetnode a'⟧ ⟹ a = a'" 
  and Main_no_call_target:"⟦valid_edge a; kind a = Q:r↪⇘Main⇙f⟧ ⟹ False" 
  and Main_no_return_source:"⟦valid_edge a; kind a = Q'↩⇘Main⇙f'⟧ ⟹ False" 
  and callee_in_procs: 
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ ∃ins outs. (p,ins,outs) ∈ set procs" 
  and get_proc_intra:"⟦valid_edge a; intra_kind(kind a)⟧
    ⟹ get_proc (sourcenode a) = get_proc (targetnode a)" 
  and get_proc_call:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_proc (targetnode a) = p"
  and get_proc_return:
    "⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ ⟹ get_proc (sourcenode a) = p"
  and call_edges_only:"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ 
    ⟹ ∀a'. valid_edge a' ∧ targetnode a' = targetnode a ⟶ 
            (∃Qx rx fsx. kind a' = Qx:rx↪⇘p⇙fsx)"
  and return_edges_only:"⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ 
    ⟹ ∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a ⟶ 
            (∃Qx fx. kind a' = Qx↩⇘p⇙fx)" 
  and get_return_edge_call:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_return_edges a ≠ {}" 
  and get_return_edges_valid:
    "⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ valid_edge a'" 
  and only_call_get_return_edges:
    "⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ ∃Q r p fs. kind a = Q:r↪⇘p⇙fs" 
  and call_return_edges:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a⟧ 
    ⟹ ∃Q' f'. kind a' = Q'↩⇘p⇙f'" 
  and return_needs_call: "⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧
    ⟹ ∃!a'. valid_edge a' ∧ (∃Q r fs. kind a' = Q:r↪⇘p⇙fs) ∧ a ∈ get_return_edges a'"
  and intra_proc_additional_edge: 
    "⟦valid_edge a; a' ∈ get_return_edges a⟧
    ⟹ ∃a''. valid_edge a'' ∧ sourcenode a'' = targetnode a ∧ 
              targetnode a'' = sourcenode a' ∧ kind a'' = (λcf. False)⇩√"
  and call_return_node_edge: 
  "⟦valid_edge a; a' ∈ get_return_edges a⟧
    ⟹ ∃a''. valid_edge a'' ∧ sourcenode a'' = sourcenode a ∧ 
             targetnode a'' = targetnode a' ∧ kind a'' = (λcf. False)⇩√"
  and call_only_one_intra_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ 
    ⟹ ∃!a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧ intra_kind(kind a')"
 and return_only_one_intra_edge:
    "⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ 
    ⟹ ∃!a'. valid_edge a' ∧ targetnode a' = targetnode a ∧ intra_kind(kind a')"
  and same_proc_call_unique_target:
    "⟦valid_edge a; valid_edge a'; kind a = Q⇩1:r⇩1↪⇘p⇙fs⇩1;  kind a' = Q⇩2:r⇩2↪⇘p⇙fs⇩2⟧
    ⟹ targetnode a = targetnode a'"
  and unique_callers:"distinct_fst procs" 
  and distinct_formal_ins:"(p,ins,outs) ∈ set procs ⟹ distinct ins"
  and distinct_formal_outs:"(p,ins,outs) ∈ set procs ⟹ distinct outs"

begin


lemma get_proc_get_return_edge:
  assumes "valid_edge a" and "a' ∈ get_return_edges a"
  shows "get_proc (sourcenode a) = get_proc (targetnode a')"
proof -
  from assms obtain ax where "valid_edge ax" and "sourcenode a = sourcenode ax"
    and "targetnode a' = targetnode ax" and "intra_kind(kind ax)"
    by(auto dest:call_return_node_edge simp:intra_kind_def)
  thus ?thesis by(fastforce intro:get_proc_intra)
qed


lemma call_intra_edge_False:
  assumes "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "valid_edge a'" 
  and "sourcenode a = sourcenode a'" and "intra_kind(kind a')"
  shows "kind a' = (λcf. False)⇩√"
proof -
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain ax where "ax ∈ get_return_edges a"
    by(fastforce dest:get_return_edge_call)
  with ‹valid_edge a› obtain a'' where "valid_edge a''" 
    and "sourcenode a'' = sourcenode a" and "kind a'' = (λcf. False)⇩√"
    by(fastforce dest:call_return_node_edge)
  from ‹kind a'' = (λcf. False)⇩√› have "intra_kind(kind a'')" 
    by(simp add:intra_kind_def)
  with assms ‹valid_edge a''› ‹sourcenode a'' = sourcenode a› 
    ‹kind a'' = (λcf. False)⇩√›
  show ?thesis by(fastforce dest:call_only_one_intra_edge)
qed


lemma formal_in_THE: 
  "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; (p,ins,outs) ∈ set procs⟧
  ⟹ (THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins"
by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers)

lemma formal_out_THE: 
  "⟦valid_edge a; kind a = Q↩⇘p⇙f; (p,ins,outs) ∈ set procs⟧
  ⟹ (THE outs. ∃ins. (p,ins,outs) ∈ set procs) = outs"
by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers)


subsubsection ‹Transfer and predicate functions›

fun params :: "(('var ⇀ 'val) ⇀ 'val) list ⇒ ('var ⇀ 'val) ⇒ 'val option list"
where "params [] cf = []"
  | "params (f#fs) cf = (f cf)#params fs cf"


lemma params_nth: 
  "i < length fs ⟹ (params fs cf)!i = (fs!i) cf"
by(induct fs arbitrary:i,auto,case_tac i,auto)


lemma [simp]:"length (params fs cf) = length fs"
  by(induct fs) auto


fun transfer :: "('var,'val,'ret,'pname) edge_kind ⇒ (('var ⇀ 'val) × 'ret) list ⇒ 
  (('var ⇀ 'val) × 'ret) list"
where "transfer (⇑f) (cf#cfs)    = (f (fst cf),snd cf)#cfs"
  | "transfer (Q)⇩√ (cf#cfs)      = (cf#cfs)"
  | "transfer (Q:r↪⇘p⇙fs) (cf#cfs) = 
       (let ins = THE ins. ∃outs. (p,ins,outs) ∈ set procs in
                            (Map.empty(ins [:=] params fs (fst cf)),r)#cf#cfs)"
  | "transfer (Q↩⇘p⇙f )(cf#cfs)    = (case cfs of [] ⇒ []
                                 | cf'#cfs' ⇒ (f (fst cf) (fst cf'),snd cf')#cfs')"
  | "transfer et [] = []"

fun transfers :: "('var,'val,'ret,'pname) edge_kind list ⇒ (('var ⇀ 'val) × 'ret) list ⇒
                  (('var ⇀ 'val) × 'ret) list"
where "transfers [] s   = s"
  | "transfers (et#ets) s = transfers ets (transfer et s)"


fun pred :: "('var,'val,'ret,'pname) edge_kind ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
where "pred (⇑f) (cf#cfs) = True"
  | "pred (Q)⇩√ (cf#cfs)   = Q (fst cf)"
  | "pred (Q:r↪⇘p⇙fs) (cf#cfs) = Q (fst cf,r)"
  | "pred (Q↩⇘p⇙f) (cf#cfs) = (Q cf ∧ cfs ≠ [])"
  | "pred et [] = False"

fun preds :: "('var,'val,'ret,'pname) edge_kind list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
where "preds [] s   = True"
  | "preds (et#ets) s = (pred et s ∧ preds ets (transfer et s))"


lemma transfers_split:
  "(transfers (ets@ets') s) = (transfers ets' (transfers ets s))"
by(induct ets arbitrary:s) auto

lemma preds_split:
  "(preds (ets@ets') s) = (preds ets s ∧ preds ets' (transfers ets s))"
by(induct ets arbitrary:s) auto


abbreviation state_val :: "(('var ⇀ 'val) × 'ret) list ⇒ 'var ⇀ 'val"
  where "state_val s V ≡ (fst (hd s)) V"


subsubsection ‹‹valid_node››

definition valid_node :: "'node ⇒ bool"
  where "valid_node n ≡ 
  (∃a. valid_edge a ∧ (n = sourcenode a ∨ n = targetnode a))"

lemma [simp]: "valid_edge a ⟹ valid_node (sourcenode a)"
  by(fastforce simp:valid_node_def)

lemma [simp]: "valid_edge a ⟹ valid_node (targetnode a)"
  by(fastforce simp:valid_node_def)



subsection ‹CFG paths›

inductive path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
  ("_ -_→* _" [51,0,0] 80)
where 
  empty_path:"valid_node n ⟹ n -[]→* n"

  | Cons_path:
  "⟦n'' -as→* n'; valid_edge a; sourcenode a = n; targetnode a = n''⟧
    ⟹ n -a#as→* n'"


lemma path_valid_node:
  assumes "n -as→* n'" shows "valid_node n" and "valid_node n'"
  using ‹n -as→* n'›
  by(induct rule:path.induct,auto)

lemma empty_path_nodes [dest]:"n -[]→* n' ⟹ n = n'"
  by(fastforce elim:path.cases)

lemma path_valid_edges:"n -as→* n' ⟹ ∀a ∈ set as. valid_edge a"
by(induct rule:path.induct) auto


lemma path_edge:"valid_edge a ⟹ sourcenode a -[a]→* targetnode a"
  by(fastforce intro:Cons_path empty_path)


lemma path_Append:"⟦n -as→* n''; n'' -as'→* n'⟧ 
  ⟹ n -as@as'→* n'"
by(induct rule:path.induct,auto intro:Cons_path)


lemma path_split:
  assumes "n -as@a#as'→* n'"
  shows "n -as→* sourcenode a" and "valid_edge a" and "targetnode a -as'→* n'"
  using ‹n -as@a#as'→* n'›
proof(induct as arbitrary:n)
  case Nil case 1
  thus ?case by(fastforce elim:path.cases intro:empty_path)
next
  case Nil case 2
  thus ?case by(fastforce elim:path.cases intro:path_edge)
next
  case Nil case 3
  thus ?case by(fastforce elim:path.cases)
next
  case (Cons ax asx) 
  note IH1 = ‹⋀n. n -asx@a#as'→* n' ⟹ n -asx→* sourcenode a›
  note IH2 = ‹⋀n. n -asx@a#as'→* n' ⟹ valid_edge a›
  note IH3 = ‹⋀n. n -asx@a#as'→* n' ⟹ targetnode a -as'→* n'›
  { case 1 
    hence "sourcenode ax = n" and "targetnode ax -asx@a#as'→* n'" and "valid_edge ax"
      by(auto elim:path.cases)
    from IH1[OF ‹ targetnode ax -asx@a#as'→* n'›] 
    have "targetnode ax -asx→* sourcenode a" .
    with ‹sourcenode ax = n› ‹valid_edge ax› show ?case by(fastforce intro:Cons_path)
  next
    case 2 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
    from IH2[OF this] show ?case .
  next
    case 3 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
    from IH3[OF this] show ?case .
  }
qed


lemma path_split_Cons:
  assumes "n -as→* n'" and "as ≠ []"
  obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
  and "valid_edge a'" and "targetnode a' -as'→* n'"
proof(atomize_elim)
  from ‹as ≠ []› obtain a' as' where "as = a'#as'" by(cases as) auto
  with ‹n -as→* n'› have "n -[]@a'#as'→* n'" by simp
  hence "n -[]→* sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(rule path_split)+
  from ‹n -[]→* sourcenode a'› have "n = sourcenode a'" by fast
  with ‹as = a'#as'› ‹valid_edge a'› ‹targetnode a' -as'→* n'›
  show "∃a' as'. as = a'#as' ∧ n = sourcenode a' ∧ valid_edge a' ∧ 
                 targetnode a' -as'→* n'"
    by fastforce
qed


lemma path_split_snoc:
  assumes "n -as→* n'" and "as ≠ []"
  obtains a' as' where "as = as'@[a']" and "n -as'→* sourcenode a'"
  and "valid_edge a'" and "n' = targetnode a'"
proof(atomize_elim)
  from ‹as ≠ []› obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto
  with ‹n -as→* n'› have "n -as'@a'#[]→* n'" by simp
  hence "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' -[]→* n'"
    by(rule path_split)+
  from ‹targetnode a' -[]→* n'› have "n' = targetnode a'" by fast
  with ‹as = as'@[a']› ‹valid_edge a'› ‹n -as'→* sourcenode a'›
  show "∃as' a'. as = as'@[a'] ∧ n -as'→* sourcenode a' ∧ valid_edge a' ∧ 
                 n' = targetnode a'"
    by fastforce
qed


lemma path_split_second:
  assumes "n -as@a#as'→* n'" shows "sourcenode a -a#as'→* n'"
proof -
  from ‹n -as@a#as'→* n'› have "valid_edge a" and "targetnode a -as'→* n'"
    by(auto intro:path_split)
  thus ?thesis by(fastforce intro:Cons_path)
qed


lemma path_Entry_Cons:
  assumes "(_Entry_) -as→* n'" and "n' ≠ (_Entry_)"
  obtains n a where "sourcenode a = (_Entry_)" and "targetnode a = n"
  and "n -tl as→* n'" and "valid_edge a" and "a = hd as"
proof(atomize_elim)
  from ‹(_Entry_) -as→* n'› ‹n' ≠ (_Entry_)› have "as ≠ []"
    by(cases as,auto elim:path.cases)
  with ‹(_Entry_) -as→* n'› obtain a' as' where "as = a'#as'" 
    and "(_Entry_) = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(erule path_split_Cons)
  thus "∃a n. sourcenode a = (_Entry_) ∧ targetnode a = n ∧ n -tl as→* n' ∧ 
              valid_edge a ∧ a = hd as"
  by fastforce
qed


lemma path_det:
  "⟦n -as→* n'; n -as→* n''⟧ ⟹ n' = n''"
proof(induct as arbitrary:n)
  case Nil thus ?case by(auto elim:path.cases)
next
  case (Cons a' as')
  note IH = ‹⋀n. ⟦n -as'→* n'; n -as'→* n''⟧ ⟹ n' = n''›
  from ‹n -a'#as'→* n'› have "targetnode a' -as'→* n'" 
    by(fastforce elim:path_split_Cons)
  from ‹n -a'#as'→* n''› have "targetnode a' -as'→* n''" 
    by(fastforce elim:path_split_Cons)
  from IH[OF ‹targetnode a' -as'→* n'› this] show ?thesis .
qed


definition
  sourcenodes :: "'edge list ⇒ 'node list"
  where "sourcenodes xs ≡ map sourcenode xs"

definition
  kinds :: "'edge list ⇒ ('var,'val,'ret,'pname) edge_kind list"
  where "kinds xs ≡ map kind xs"

definition
  targetnodes :: "'edge list ⇒ 'node list"
  where "targetnodes xs ≡ map targetnode xs"


lemma path_sourcenode:
  "⟦n -as→* n'; as ≠ []⟧ ⟹ hd (sourcenodes as) = n"
by(fastforce elim:path_split_Cons simp:sourcenodes_def)



lemma path_targetnode:
  "⟦n -as→* n'; as ≠ []⟧ ⟹ last (targetnodes as) = n'"
by(fastforce elim:path_split_snoc simp:targetnodes_def)



lemma sourcenodes_is_n_Cons_butlast_targetnodes:
  "⟦n -as→* n'; as ≠ []⟧ ⟹ 
  sourcenodes as = n#(butlast (targetnodes as))"
proof(induct as arbitrary:n)
  case Nil thus ?case by simp
next
  case (Cons a' as')
  note IH = ‹⋀n. ⟦n -as'→* n'; as' ≠ []⟧
            ⟹ sourcenodes as' = n#(butlast (targetnodes as'))›
  from ‹n -a'#as'→* n'› have "n = sourcenode a'" and "targetnode a' -as'→* n'"
    by(auto elim:path_split_Cons)
  show ?case
  proof(cases "as' = []")
    case True
    with ‹targetnode a' -as'→* n'› have "targetnode a' = n'" by fast
    with True ‹n = sourcenode a'› show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  next
    case False
    from IH[OF ‹targetnode a' -as'→* n'› this] 
    have "sourcenodes as' = targetnode a' # butlast (targetnodes as')" .
    with ‹n = sourcenode a'› False show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  qed
qed



lemma targetnodes_is_tl_sourcenodes_App_n':
  "⟦n -as→* n'; as ≠ []⟧ ⟹ 
    targetnodes as = (tl (sourcenodes as))@[n']"
proof(induct as arbitrary:n' rule:rev_induct)
  case Nil thus ?case by simp
next
  case (snoc a' as')
  note IH = ‹⋀n'. ⟦n -as'→* n'; as' ≠ []⟧
    ⟹ targetnodes as' = tl (sourcenodes as') @ [n']›
  from ‹n -as'@[a']→* n'› have "n -as'→* sourcenode a'" and "n' = targetnode a'"
    by(auto elim:path_split_snoc)
  show ?case
  proof(cases "as' = []")
    case True
    with ‹n -as'→* sourcenode a'› have "n = sourcenode a'" by fast
    with True ‹n' = targetnode a'› show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  next
    case False
    from IH[OF ‹n -as'→* sourcenode a'› this]
    have "targetnodes as' = tl (sourcenodes as')@[sourcenode a']" .
    with ‹n' = targetnode a'› False show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  qed
qed


subsubsection ‹Intraprocedural paths›

definition intra_path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool" 
  ("_ -_→⇩ι* _" [51,0,0] 80)
where "n -as→⇩ι* n' ≡ n -as→* n' ∧ (∀a ∈ set as. intra_kind(kind a))"

lemma intra_path_get_procs:
  assumes "n -as→⇩ι* n'" shows "get_proc n = get_proc n'"
proof -
  from ‹n -as→⇩ι* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind(kind a)"
    by(simp_all add:intra_path_def)
  thus ?thesis
  proof(induct as arbitrary:n)
    case Nil thus ?case by fastforce
  next
    case (Cons a' as')
    note IH = ‹⋀n. ⟦n -as'→* n'; ∀a∈set as'. intra_kind (kind a)⟧
      ⟹ get_proc n = get_proc n'›
    from ‹∀a∈set (a'#as'). intra_kind (kind a)›
    have "intra_kind(kind a')" and "∀a∈set as'. intra_kind (kind a)" by simp_all
    from ‹n -a'#as'→* n'› have "sourcenode a' = n" and "valid_edge a'"
      and "targetnode a' -as'→* n'" by(auto elim:path.cases)
    from IH[OF ‹targetnode a' -as'→* n'› ‹∀a∈set as'. intra_kind (kind a)›]
    have "get_proc (targetnode a') = get_proc n'" .
    from ‹valid_edge a'› ‹intra_kind(kind a')› 
    have "get_proc (sourcenode a') = get_proc (targetnode a')"
      by(rule get_proc_intra)
    with ‹sourcenode a' = n› ‹get_proc (targetnode a') = get_proc n'›
    show ?case by simp
  qed
qed


lemma intra_path_Append:
  "⟦n -as→⇩ι* n''; n'' -as'→⇩ι* n'⟧ ⟹ n -as@as'→⇩ι* n'"
by(fastforce intro:path_Append simp:intra_path_def)


lemma get_proc_get_return_edges: 
  assumes "valid_edge a" and "a' ∈ get_return_edges a"
  shows "get_proc(targetnode a) = get_proc(sourcenode a')"
proof -
  from ‹valid_edge a› ‹a' ∈ get_return_edges a›
  obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
    and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
    by(fastforce dest:intra_proc_additional_edge)
  from ‹valid_edge a''› ‹kind a'' = (λcf. False)⇩√›
  have "get_proc(sourcenode a'') = get_proc(targetnode a'')"
    by(fastforce intro:get_proc_intra simp:intra_kind_def)
  with ‹sourcenode a'' = targetnode a› ‹targetnode a'' = sourcenode a'›
  show ?thesis by simp
qed


subsubsection ‹Valid paths›

declare conj_cong[fundef_cong]

fun valid_path_aux :: "'edge list ⇒ 'edge list ⇒ bool"
  where "valid_path_aux cs [] ⟷ True"
  | "valid_path_aux cs (a#as) ⟷ 
       (case (kind a) of Q:r↪⇘p⇙fs ⇒ valid_path_aux (a#cs) as
                       | Q↩⇘p⇙f ⇒ case cs of [] ⇒ valid_path_aux [] as
                                     | c'#cs' ⇒ a ∈ get_return_edges c' ∧
                                                 valid_path_aux cs' as
                       |    _ ⇒ valid_path_aux cs as)"


lemma vpa_induct [consumes 1,case_names vpa_empty vpa_intra vpa_Call vpa_ReturnEmpty
  vpa_ReturnCons]:
  assumes major: "valid_path_aux xs ys"
  and rules: "⋀cs. P cs []"
    "⋀cs a as. ⟦intra_kind(kind a); valid_path_aux cs as; P cs as⟧ ⟹ P cs (a#as)"
    "⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; valid_path_aux (a#cs) as; P (a#cs) as⟧ 
      ⟹ P cs (a#as)"
    "⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; cs = []; valid_path_aux [] as; P [] as⟧ 
      ⟹ P cs (a#as)"
    "⋀cs a as Q p f c' cs' . ⟦kind a = Q↩⇘p⇙f; cs = c'#cs'; valid_path_aux cs' as;
                              a ∈ get_return_edges c'; P cs' as⟧
     ⟹ P cs (a#as)"
  shows "P xs ys"
using major
apply(induct ys arbitrary: xs)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)


lemma valid_path_aux_intra_path:
  "∀a ∈ set as. intra_kind(kind a) ⟹ valid_path_aux cs as"
by(induct as,auto simp:intra_kind_def)


lemma valid_path_aux_callstack_prefix:
  "valid_path_aux (cs@cs') as ⟹ valid_path_aux cs as"
proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpa_induct)
  case vpa_empty thus ?case by simp
next
  case (vpa_intra a as)
  hence "valid_path_aux cs as" by simp
  with ‹intra_kind (kind a)› show ?case by(cases "kind a",auto simp:intra_kind_def)
next
  case (vpa_Call a as Q r p fs cs'' cs')
  note IH = ‹⋀xs ys. a#cs''@cs' = xs@ys ⟹ valid_path_aux xs as›
  have "a#cs''@cs' = (a#cs'')@cs'" by simp
  from IH[OF this] have "valid_path_aux (a#cs'') as" .
  with ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp
next
  case (vpa_ReturnEmpty a as Q p f cs'' cs')
  hence "valid_path_aux cs'' as" by simp
  with ‹kind a = Q↩⇘p⇙f› ‹cs''@cs' = []› show ?case by simp
next
  case (vpa_ReturnCons a as Q p f c' cs' csx csx')
  note IH = ‹⋀xs ys. cs' = xs@ys ⟹ valid_path_aux xs as›
  from ‹csx@csx' = c'#cs'› 
  have "csx = [] ∧ csx' = c'#cs' ∨ (∃zs. csx = c'#zs ∧ zs@csx' = cs')"
    by(simp add:append_eq_Cons_conv)
  thus ?case
  proof
    assume "csx = [] ∧ csx' = c'#cs'"
    hence "csx = []" and "csx' = c'#cs'" by simp_all
    from ‹csx' = c'#cs'› have "cs' = []@tl csx'" by simp
    from IH[OF this] have "valid_path_aux [] as" .
    with ‹csx = []› ‹kind a = Q↩⇘p⇙f› show ?thesis by simp
  next
    assume "∃zs. csx = c'#zs ∧ zs@csx' = cs'"
    then obtain zs where "csx = c'#zs" and "cs' = zs@csx'" by auto
    from IH[OF ‹cs' = zs@csx'›] have "valid_path_aux zs as" .
    with ‹csx = c'#zs› ‹kind a = Q↩⇘p⇙f› ‹a ∈ get_return_edges c'› 
    show ?thesis by simp
  qed
qed


fun upd_cs :: "'edge list ⇒ 'edge list ⇒ 'edge list"
  where "upd_cs cs [] = cs"
  | "upd_cs cs (a#as) =
       (case (kind a) of Q:r↪⇘p⇙fs ⇒ upd_cs (a#cs) as
                       | Q↩⇘p⇙f ⇒ case cs of [] ⇒ upd_cs cs as
                                      | c'#cs' ⇒ upd_cs cs' as
                       |    _ ⇒ upd_cs cs as)"


lemma upd_cs_empty [dest]:
  "upd_cs cs [] = [] ⟹ cs = []"
by(cases cs) auto


lemma upd_cs_intra_path:
  "∀a ∈ set as. intra_kind(kind a) ⟹ upd_cs cs as = cs"
by(induct as,auto simp:intra_kind_def)


lemma upd_cs_Append:
  "⟦upd_cs cs as = cs'; upd_cs cs' as' = cs''⟧ ⟹ upd_cs cs (as@as') = cs''"
by(induct as arbitrary:cs,auto split:edge_kind.split list.split)


lemma upd_cs_empty_split:
  assumes "upd_cs cs as = []" and "cs ≠ []" and "as ≠ []"
  obtains xs ys where "as = xs@ys" and "xs ≠ []" and "upd_cs cs xs = []"
  and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
  and "upd_cs [] ys = []"
proof(atomize_elim)
  from ‹upd_cs cs as = []› ‹cs ≠ []› ‹as ≠ []›
  show "∃xs ys. as = xs@ys ∧ xs ≠ [] ∧ upd_cs cs xs = [] ∧ 
             (∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []) ∧ 
             upd_cs [] ys = []"
  proof(induct as arbitrary:cs)
    case Nil thus ?case by simp
  next
    case (Cons a' as')
    note IH = ‹⋀cs. ⟦upd_cs cs as' = []; cs ≠ []; as' ≠ []⟧
      ⟹ ∃xs ys. as' = xs@ys ∧ xs ≠ [] ∧ upd_cs cs xs = [] ∧
                 (∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []) ∧ 
                 upd_cs [] ys = []›
    show ?case
    proof(cases "kind a'" rule:edge_kind_cases)
      case Intra
      with ‹upd_cs cs (a'#as') = []› have "upd_cs cs as' = []"
        by(fastforce simp:intra_kind_def)
      with ‹cs ≠ []› have "as' ≠ []" by fastforce
      from IH[OF ‹upd_cs cs as' = []› ‹cs ≠ []› this] obtain xs ys where "as' = xs@ys"
        and "xs ≠ []" and "upd_cs cs xs = []" and "upd_cs [] ys = []"
        and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []" by blast
      from ‹upd_cs cs xs = []› Intra have "upd_cs cs (a'#xs) = []"
        by(fastforce simp:intra_kind_def)
      from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []› ‹xs ≠ []› Intra
      have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
        apply auto
        apply(case_tac xs') apply(auto simp:intra_kind_def)
        by(erule_tac x="[]" in allE,fastforce)+
      with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
      show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
    next
      case (Call Q p f)
      with ‹upd_cs cs (a'#as') = []› have "upd_cs (a'#cs) as' = []" by simp
      with ‹cs ≠ []› have "as' ≠ []" by fastforce
      from IH[OF ‹upd_cs (a'#cs) as' = []› _ this] obtain xs ys where "as' = xs@ys"
        and "xs ≠ []" and "upd_cs (a'#cs) xs = []" and "upd_cs [] ys = []"
        and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs (a'#cs) xs' ≠ []" by blast
      from ‹upd_cs (a'#cs) xs = []› Call have "upd_cs cs (a'#xs) = []" by simp
      from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs (a'#cs) xs' ≠ []› 
        ‹xs ≠ []› ‹cs ≠ []› Call
      have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
        by auto(case_tac xs',auto)
      with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
      show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
    next
      case (Return Q p f)
      with ‹upd_cs cs (a'#as') = []› ‹cs ≠ []› obtain c' cs' where "cs = c'#cs'"
        and "upd_cs cs' as' = []" by(cases cs) auto
      show ?thesis
      proof(cases "cs' = []")
        case True
        with ‹cs = c'#cs'› ‹upd_cs cs' as' = []› Return show ?thesis
          apply(rule_tac x="[a']" in exI) apply clarsimp
          by(case_tac xs') auto
      next
        case False
        with ‹upd_cs cs' as' = []› have "as' ≠ []" by fastforce
        from IH[OF ‹upd_cs cs' as' = []› False this] obtain xs ys where "as' = xs@ys"
          and "xs ≠ []" and "upd_cs cs' xs = []" and "upd_cs [] ys = []"
          and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs' xs' ≠ []" by blast
        from ‹upd_cs cs' xs = []› ‹cs = c'#cs'› Return have "upd_cs cs (a'#xs) = []"
          by simp
        from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs' xs' ≠ []›
          ‹xs ≠ []› ‹cs = c'#cs'› Return
        have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
          by auto(case_tac xs',auto)
        with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
        show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
      qed
    qed
  qed
qed


lemma upd_cs_snoc_Return_Cons:
  assumes "kind a = Q↩⇘p⇙f"
  shows "upd_cs cs as = c'#cs' ⟹ upd_cs cs (as@[a]) = cs'"
proof(induct as arbitrary:cs)
  case Nil
  with ‹kind a = Q↩⇘p⇙f› have "upd_cs cs [a] = cs'" by simp
 thus ?case by simp
next
  case (Cons a' as')
  note IH = ‹⋀cs. upd_cs cs as' = c'#cs' ⟹ upd_cs cs (as'@[a]) = cs'›
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    with ‹upd_cs cs (a'#as') = c'#cs'›
    have "upd_cs cs as' = c'#cs'" by(fastforce simp:intra_kind_def)
    from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" .
    with Intra show ?thesis by(fastforce simp:intra_kind_def)
  next
    case Call
    with ‹upd_cs cs (a'#as') = c'#cs'›
    have "upd_cs (a'#cs) as' = c'#cs'" by simp
    from IH[OF this] have "upd_cs (a'#cs) (as'@[a]) = cs'" .
    with Call show ?thesis by simp
  next
    case Return
    show ?thesis
    proof(cases cs)
      case Nil
      with ‹upd_cs cs (a'#as') = c'#cs'› Return
      have "upd_cs cs as' = c'#cs'" by simp
      from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" .
      with Nil Return show ?thesis by simp
    next
      case (Cons cx csx)
      with ‹upd_cs cs (a'#as') = c'#cs'› Return
      have "upd_cs csx as' = c'#cs'" by simp
      from IH[OF this] have "upd_cs csx (as'@[a]) = cs'" .
      with Cons Return show ?thesis by simp
    qed
  qed
qed


lemma upd_cs_snoc_Call:
  assumes "kind a = Q:r↪⇘p⇙fs"
  shows "upd_cs cs (as@[a]) = a#(upd_cs cs as)"
proof(induct as arbitrary:cs)
  case Nil
  with ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp
next
  case (Cons a' as')
  note IH = ‹⋀cs. upd_cs cs (as'@[a]) = a#upd_cs cs as'›
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra 
    with IH[of cs] show ?thesis by(fastforce simp:intra_kind_def)
  next
    case Call
    with IH[of "a'#cs"] show ?thesis by simp
  next
    case Return
    show ?thesis
    proof(cases cs)
      case Nil
      with IH[of "[]"] Return show ?thesis by simp
    next
      case (Cons cx csx)
      with IH[of csx] Return show ?thesis by simp
    qed
  qed
qed





lemma valid_path_aux_split:
  assumes "valid_path_aux cs (as@as')"
  shows "valid_path_aux cs as" and "valid_path_aux (upd_cs cs as) as'"
  using ‹valid_path_aux cs (as@as')›
proof(induct cs "as@as'" arbitrary:as as' rule:vpa_induct)
  case (vpa_intra cs a as as'')
  note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux cs xs›
  note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs cs xs) ys›
  { case 1
    from vpa_intra
    have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = [] ∧ a#as = as'"
      thus ?thesis by simp
    next
      assume "∃xs. a#xs = as'' ∧ as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH1[OF ‹as = xs@as'›] have "valid_path_aux cs xs" .
      with ‹a#xs = as''› ‹intra_kind (kind a)›
      show ?thesis by(fastforce simp:intra_kind_def)
    qed
  next
    case 2
    from vpa_intra
    have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = [] ∧ a#as = as'"
      hence "as = []@tl as'" by(cases as') auto
      from IH2[OF this] have "valid_path_aux (upd_cs cs []) (tl as')" by simp
      with ‹as'' = [] ∧ a#as = as'› ‹intra_kind (kind a)›
      show ?thesis by(fastforce simp:intra_kind_def)
    next
      assume "∃xs. a#xs = as'' ∧ as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs cs xs) as'" .
      from ‹a#xs = as''› ‹intra_kind (kind a)› 
      have "upd_cs cs xs = upd_cs cs as''" by(fastforce simp:intra_kind_def)
      with ‹valid_path_aux (upd_cs cs xs) as'›
      show ?thesis by simp
    qed
  }
next
  case (vpa_Call cs a as Q r p fs as'')
  note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (a#cs) xs›
  note IH2 = ‹⋀xs ys. as = xs@ys ⟹   valid_path_aux (upd_cs (a#cs) xs) ys›
  { case 1
    from vpa_Call
    have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = [] ∧ a#as = as'"
      thus ?thesis by simp
    next
      assume "∃xs. a#xs = as'' ∧ as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH1[OF ‹as = xs@as'›] have "valid_path_aux (a#cs) xs" .
      with ‹a#xs = as''›[THEN sym] ‹kind a = Q:r↪⇘p⇙fs›
      show ?thesis by simp
    qed
  next
    case 2
    from vpa_Call
    have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = [] ∧ a#as = as'"
      hence "as = []@tl as'" by(cases as') auto
      from IH2[OF this] have "valid_path_aux (upd_cs (a#cs) []) (tl as')" .
      with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q:r↪⇘p⇙fs›
      show ?thesis by clarsimp
    next
      assume "∃xs. a#xs = as'' ∧ as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs (a # cs) xs) as'" .
      with ‹a#xs = as''›[THEN sym]  ‹kind a = Q:r↪⇘p⇙fs›
      show ?thesis by simp
    qed
  }
next
  case (vpa_ReturnEmpty cs a as Q p f as'')
  note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux [] xs›
  note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs [] xs) ys›
  { case 1
    from vpa_ReturnEmpty
    have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = [] ∧ a#as = as'"
      thus ?thesis by simp
    next
      assume "∃xs. a#xs = as'' ∧ as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH1[OF ‹as = xs@as'›] have "valid_path_aux [] xs" .
      with ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = []›
      show ?thesis by simp
    qed
  next
    case 2
    from vpa_ReturnEmpty
    have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = [] ∧ a#as = as'"
      hence "as = []@tl as'" by(cases as') auto
      from IH2[OF this] have "valid_path_aux [] (tl as')" by simp
      with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q↩⇘p⇙f› ‹cs = []›
      show ?thesis by fastforce
    next
      assume "∃xs. a#xs = as'' ∧ as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs [] xs) as'" .
      from ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = []›
      have "upd_cs [] xs = upd_cs cs as''" by simp
      with ‹valid_path_aux (upd_cs [] xs) as'› show ?thesis by simp
    qed
  }
next
  case (vpa_ReturnCons cs a as Q p f c' cs' as'')
  note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux cs' xs›
  note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs cs' xs) ys›
  { case 1
    from vpa_ReturnCons
    have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = [] ∧ a#as = as'"
      thus ?thesis by simp
    next
       assume "∃xs. a#xs = as'' ∧ as = xs@as'"
       then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
       from IH1[OF ‹as = xs@as'›] have "valid_path_aux cs' xs" .
       with ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
         ‹a ∈ get_return_edges c'›
       show ?thesis by simp
     qed
   next
     case 2
     from vpa_ReturnCons
     have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = [] ∧ a#as = as'"
      hence "as = []@tl as'" by(cases as') auto
      from IH2[OF this] have "valid_path_aux (upd_cs cs' []) (tl as')" .
       with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
         ‹a ∈ get_return_edges c'›
       show ?thesis by fastforce
    next
      assume "∃xs. a#xs = as'' ∧ as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs cs' xs) as'" .
      from ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
      have "upd_cs cs' xs = upd_cs cs as''" by simp
      with ‹valid_path_aux (upd_cs cs' xs) as'› show ?thesis by simp
    qed
  }
qed simp_all


lemma valid_path_aux_Append:
  "⟦valid_path_aux cs as; valid_path_aux (upd_cs cs as) as'⟧
  ⟹ valid_path_aux cs (as@as')"
by(induct rule:vpa_induct,auto simp:intra_kind_def)


lemma vpa_snoc_Call:
  assumes "kind a = Q:r↪⇘p⇙fs"
  shows "valid_path_aux cs as ⟹ valid_path_aux cs (as@[a])"
proof(induct rule:vpa_induct)
  case (vpa_empty cs)
  from ‹kind a = Q:r↪⇘p⇙fs› have "valid_path_aux cs [a]" by simp
  thus ?case by simp
next
  case (vpa_intra cs a' as')
  from ‹valid_path_aux cs (as'@[a])› ‹intra_kind (kind a')›
  have "valid_path_aux cs (a'#(as'@[a]))"
    by(fastforce simp:intra_kind_def)
  thus ?case by simp
next
  case (vpa_Call cs a' as' Q' r' p' fs')
  from ‹valid_path_aux (a'#cs) (as'@[a])› ‹kind a' = Q':r'↪⇘p'⇙fs'›
  have "valid_path_aux cs (a'#(as'@[a]))" by simp
  thus ?case by simp
next
  case (vpa_ReturnEmpty cs a' as' Q' p' f')
  from ‹valid_path_aux [] (as'@[a])› ‹kind a' = Q'↩⇘p'⇙f'› ‹cs = []›
  have "valid_path_aux cs (a'#(as'@[a]))" by simp
  thus ?case by simp
next
  case (vpa_ReturnCons cs a' as' Q' p' f' c' cs')
  from ‹valid_path_aux cs' (as'@[a])› ‹kind a' = Q'↩⇘p'⇙f'› ‹cs = c'#cs'›
    ‹a' ∈ get_return_edges c'›
  have "valid_path_aux cs (a'#(as'@[a]))" by simp
  thus ?case by simp
qed



definition valid_path :: "'edge list ⇒ bool"
  where "valid_path as ≡ valid_path_aux [] as"


lemma valid_path_aux_valid_path:
  "valid_path_aux cs as ⟹ valid_path as"
by(fastforce intro:valid_path_aux_callstack_prefix simp:valid_path_def)

lemma valid_path_split:
  assumes "valid_path (as@as')" shows "valid_path as" and "valid_path as'"
  using ‹valid_path (as@as')›
  apply(auto simp:valid_path_def)
   apply(erule valid_path_aux_split)
  apply(drule valid_path_aux_split(2))
  by(fastforce intro:valid_path_aux_callstack_prefix)



definition valid_path' :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
  ("_ -_→⇩√* _" [51,0,0] 80)
where vp_def:"n -as→⇩√* n' ≡ n -as→* n' ∧ valid_path as"


lemma intra_path_vp:
  assumes "n -as→⇩ι* n'" shows "n -as→⇩√* n'"
proof -
  from ‹n -as→⇩ι* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind(kind a)"
    by(simp_all add:intra_path_def)
  from ‹∀a ∈ set as. intra_kind(kind a)› have "valid_path_aux [] as"
    by(rule valid_path_aux_intra_path)
  thus ?thesis using ‹n -as→* n'› by(simp add:vp_def valid_path_def)
qed


lemma vp_split_Cons:
  assumes "n -as→⇩√* n'" and "as ≠ []"
  obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
  and "valid_edge a'" and "targetnode a' -as'→⇩√* n'"
proof(atomize_elim)
  from ‹n -as→⇩√* n'› ‹as ≠ []› obtain a' as' where "as = a'#as'"
    and "n = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(fastforce elim:path_split_Cons simp:vp_def)
  from ‹n -as→⇩√* n'› have "valid_path as" by(simp add:vp_def)
  from ‹as = a'#as'› have "as = [a']@as'" by simp
  with ‹valid_path as› have "valid_path ([a']@as')" by simp
  hence "valid_path as'" by(rule valid_path_split)
  with ‹targetnode a' -as'→* n'› have "targetnode a' -as'→⇩√* n'" by(simp add:vp_def)
  with ‹as = a'#as'› ‹n = sourcenode a'› ‹valid_edge a'›
  show "∃a' as'. as = a'#as' ∧ n = sourcenode a' ∧ valid_edge a' ∧ 
                 targetnode a' -as'→⇩√* n'" by blast
qed

lemma vp_split_snoc:
  assumes "n -as→⇩√* n'" and "as ≠ []"
  obtains a' as' where "as = as'@[a']" and "n -as'→⇩√* sourcenode a'"
  and "valid_edge a'" and "n' = targetnode a'"
proof(atomize_elim)
  from ‹n -as→⇩√* n'› ‹as ≠ []› obtain a' as' where "as = as'@[a']"
    and "n -as'→* sourcenode a'" and "valid_edge a'" and "n' = targetnode a'"
    by(clarsimp simp:vp_def)(erule path_split_snoc,auto)
  from ‹n -as→⇩√* n'› ‹as = as'@[a']› have "valid_path (as'@[a'])" by(simp add:vp_def)
  hence "valid_path as'" by(rule valid_path_split)
  with ‹n -as'→* sourcenode a'› have "n -as'→⇩√* sourcenode a'" by(simp add:vp_def)
  with ‹as = as'@[a']› ‹valid_edge a'› ‹n' = targetnode a'›
  show "∃as' a'. as = as'@[a'] ∧ n -as'→⇩√* sourcenode a' ∧ valid_edge a' ∧ 
                 n' = targetnode a'"
  by blast
qed

lemma vp_split:
  assumes "n -as@a#as'→⇩√* n'"
  shows "n -as→⇩√* sourcenode a" and "valid_edge a" and "targetnode a -as'→⇩√* n'"
proof -
  from ‹n -as@a#as'→⇩√* n'› have "n -as→* sourcenode a" and "valid_edge a" 
    and "targetnode a -as'→* n'"
    by(auto intro:path_split simp:vp_def)
  from ‹n -as@a#as'→⇩√* n'› have "valid_path (as@a#as')" by(simp add:vp_def)
  hence "valid_path as" and "valid_path (a#as')" by(auto intro:valid_path_split)
  from ‹valid_path (a#as')› have "valid_path ([a]@as')" by simp
  hence "valid_path as'"  by(rule valid_path_split)
  with ‹n -as→* sourcenode a› ‹valid_path as› ‹valid_edge a› ‹targetnode a -as'→* n'›
  show "n -as→⇩√* sourcenode a" "valid_edge a" "targetnode a -as'→⇩√* n'"
    by(auto simp:vp_def)
qed

lemma vp_split_second:
  assumes "n -as@a#as'→⇩√* n'" shows "sourcenode a -a#as'→⇩√* n'"
proof -
  from ‹n -as@a#as'→⇩√* n'› have "sourcenode a -a#as'→* n'"
    by(fastforce elim:path_split_second simp:vp_def)
  from ‹n -as@a#as'→⇩√* n'› have "valid_path (as@a#as')" by(simp add:vp_def)
  hence "valid_path (a#as')" by(rule valid_path_split)
  with ‹sourcenode a -a#as'→* n'› show ?thesis by(simp add:vp_def)
qed




function valid_path_rev_aux :: "'edge list ⇒ 'edge list ⇒ bool"
  where "valid_path_rev_aux cs [] ⟷ True"
  | "valid_path_rev_aux cs (as@[a]) ⟷ 
       (case (kind a) of Q↩⇘p⇙f ⇒ valid_path_rev_aux (a#cs) as
                       | Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ valid_path_rev_aux [] as
                                     | c'#cs' ⇒ c' ∈ get_return_edges a ∧
                                                 valid_path_rev_aux cs' as
                       |    _ ⇒ valid_path_rev_aux cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order



lemma vpra_induct [consumes 1,case_names vpra_empty vpra_intra vpra_Return 
  vpra_CallEmpty vpra_CallCons]:
  assumes major: "valid_path_rev_aux xs ys"
  and rules: "⋀cs. P cs []"
    "⋀cs a as. ⟦intra_kind(kind a); valid_path_rev_aux cs as; P cs as⟧ 
      ⟹ P cs (as@[a])"
    "⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; valid_path_rev_aux (a#cs) as; P (a#cs) as⟧ 
      ⟹ P cs (as@[a])"
    "⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; cs = []; valid_path_rev_aux [] as; 
         P [] as⟧ ⟹ P cs (as@[a])"
    "⋀cs a as Q r p fs c' cs'. ⟦kind a = Q:r↪⇘p⇙fs; cs = c'#cs'; 
         valid_path_rev_aux cs' as; c' ∈ get_return_edges a; P cs' as⟧
     ⟹ P cs (as@[a])"
  shows "P xs ys"
using major
apply(induct ys arbitrary:xs rule:rev_induct)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)


lemma vpra_callstack_prefix:
  "valid_path_rev_aux (cs@cs') as ⟹ valid_path_rev_aux cs as"
proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpra_induct)
  case vpra_empty thus ?case by simp
next
  case (vpra_intra a as)
  hence "valid_path_rev_aux cs as" by simp
  with ‹intra_kind (kind a)› show ?case by(fastforce simp:intra_kind_def)
next
  case (vpra_Return a as Q p f)
  note IH = ‹⋀ds ds'. a#cs@cs' = ds@ds' ⟹ valid_path_rev_aux ds as›
  have "a#cs@cs' = (a#cs)@cs'" by simp
  from IH[OF this] have "valid_path_rev_aux (a#cs) as" .
  with ‹kind a = Q↩⇘p⇙f› show ?case by simp
next
  case (vpra_CallEmpty a as Q r p fs)
  hence "valid_path_rev_aux cs as" by simp
  with ‹kind a = Q:r↪⇘p⇙fs› ‹cs@cs' = []› show ?case by simp
next
  case (vpra_CallCons a as Q r p fs c' csx)
  note IH = ‹⋀cs cs'. csx = cs@cs' ⟹ valid_path_rev_aux cs as›
  from ‹cs@cs' = c'#csx›
  have "(cs = [] ∧ cs' = c'#csx) ∨ (∃zs. cs = c'#zs ∧ zs@cs' = csx)"
    by(simp add:append_eq_Cons_conv)
  thus ?case
  proof
    assume "cs = [] ∧ cs' = c'#csx"
    hence "cs = []" and "cs' = c'#csx" by simp_all
    from ‹cs' = c'#csx› have "csx = []@tl cs'" by simp
    from IH[OF this] have "valid_path_rev_aux [] as" .
    with ‹cs = []› ‹kind a = Q:r↪⇘p⇙fs› show ?thesis by simp
  next
    assume "∃zs. cs = c'#zs ∧ zs@cs' = csx"
    then obtain zs where "cs = c'#zs" and "csx = zs@cs'" by auto
    from IH[OF ‹csx = zs@cs'›] have "valid_path_rev_aux zs as" .
    with ‹cs = c'#zs› ‹kind a = Q:r↪⇘p⇙fs› ‹c' ∈ get_return_edges a› show ?thesis by simp
  qed
qed



function upd_rev_cs :: "'edge list ⇒ 'edge list ⇒ 'edge list"
  where "upd_rev_cs cs [] = cs"
  | "upd_rev_cs cs (as@[a]) =
       (case (kind a) of Q↩⇘p⇙f ⇒ upd_rev_cs (a#cs) as
                       | Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ upd_rev_cs cs as
                                      | c'#cs' ⇒ upd_rev_cs cs' as
                       |    _ ⇒ upd_rev_cs cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order


lemma upd_rev_cs_empty [dest]:
  "upd_rev_cs cs [] = [] ⟹ cs = []"
by(cases cs) auto


lemma valid_path_rev_aux_split:
  assumes "valid_path_rev_aux cs (as@as')"
  shows "valid_path_rev_aux cs as'" and "valid_path_rev_aux (upd_rev_cs cs as') as"
  using ‹valid_path_rev_aux cs (as@as')›
proof(induct cs "as@as'" arbitrary:as as' rule:vpra_induct)
  case (vpra_intra cs a as as'')
  note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux cs ys›
  note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs cs ys) xs›
  { case 1
    from vpra_intra
    have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = [] ∧ as@[a] = as''"
      thus ?thesis by simp
    next
      assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux cs xs" .
      with ‹xs@[a] = as'› ‹intra_kind (kind a)›
      show ?thesis by(fastforce simp:intra_kind_def)
    qed
  next
    case 2
    from vpra_intra
    have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = [] ∧ as@[a] = as''"
      hence "as = butlast as''@[]" by(cases as) auto
      from IH2[OF this] have "valid_path_rev_aux (upd_rev_cs cs []) (butlast as'')" .
      with ‹as' = [] ∧ as@[a] = as''› ‹intra_kind (kind a)›
      show ?thesis by(fastforce simp:intra_kind_def)
    next
      assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH2[OF ‹as = as''@xs›] have "valid_path_rev_aux (upd_rev_cs cs xs) as''" .
      from ‹xs@[a] = as'› ‹intra_kind (kind a)› 
      have "upd_rev_cs cs xs = upd_rev_cs cs as'" by(fastforce simp:intra_kind_def)
      with ‹valid_path_rev_aux (upd_rev_cs cs xs) as''›
      show ?thesis by simp
    qed
  }
next
  case (vpra_Return cs a as Q p f as'')
  note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (a#cs) ys›
  note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs (a#cs) ys) xs›
  { case 1
    from vpra_Return
    have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = [] ∧ as@[a] = as''"
      thus ?thesis by simp
    next
      assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux (a#cs) xs" .
      with ‹xs@[a] = as'› ‹kind a = Q↩⇘p⇙f›
      show ?thesis by fastforce
    qed
  next
    case 2
    from vpra_Return
    have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = [] ∧ as@[a] = as''"
      hence "as = butlast as''@[]" by(cases as) auto
      from IH2[OF this] 
      have "valid_path_rev_aux (upd_rev_cs (a#cs) []) (butlast as'')" .
      with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q↩⇘p⇙f›
      show ?thesis by fastforce
    next
      assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH2[OF ‹as = as''@xs›] 
      have "valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''" .
      from ‹xs@[a] = as'› ‹kind a = Q↩⇘p⇙f›
      have "upd_rev_cs (a#cs) xs = upd_rev_cs cs as'" by fastforce
      with ‹valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''›
      show ?thesis by simp
    qed
  }
next
  case (vpra_CallEmpty cs a as Q r p fs as'')
  note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux [] ys›
  note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs [] ys) xs›
  { case 1
    from vpra_CallEmpty
    have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = [] ∧ as@[a] = as''"
      thus ?thesis by simp
    next
      assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux [] xs" .
      with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []›
      show ?thesis by fastforce
    qed
  next
    case 2
    from vpra_CallEmpty
    have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = [] ∧ as@[a] = as''"
      hence "as = butlast as''@[]" by(cases as) auto
      from IH2[OF this] 
      have "valid_path_rev_aux (upd_rev_cs [] []) (butlast as'')" .
      with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []›
      show ?thesis by fastforce
    next
      assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH2[OF ‹as = as''@xs›] 
      have "valid_path_rev_aux (upd_rev_cs [] xs) as''" .
      with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []› 
      show ?thesis by fastforce
    qed
  }
next
  case (vpra_CallCons cs a as Q r p fs c' cs' as'')
  note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux cs' ys›
  note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs cs' ys) xs›
  { case 1
    from vpra_CallCons
    have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = [] ∧ as@[a] = as''"
      thus ?thesis by simp
    next
      assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux cs' xs" .
      with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'› ‹c' ∈ get_return_edges a›
      show ?thesis by fastforce
    qed
  next
    case 2
    from vpra_CallCons
    have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = [] ∧ as@[a] = as''"
      hence "as = butlast as''@[]" by(cases as) auto
      from IH2[OF this] 
      have "valid_path_rev_aux (upd_rev_cs cs' []) (butlast as'')" .
      with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'›
        ‹c' ∈ get_return_edges a› show ?thesis by fastforce
    next
      assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH2[OF ‹as = as''@xs›] 
      have "valid_path_rev_aux (upd_rev_cs cs' xs) as''" .
      with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'›
        ‹c' ∈ get_return_edges a›
      show ?thesis by fastforce
    qed
  }
qed simp_all


lemma valid_path_rev_aux_Append:
  "⟦valid_path_rev_aux cs as'; valid_path_rev_aux (upd_rev_cs cs as') as⟧
  ⟹ valid_path_rev_aux cs (as@as')"
by(induct rule:vpra_induct,
   auto simp:intra_kind_def simp del:append_assoc simp:append_assoc[THEN sym])


lemma vpra_Cons_intra:
  assumes "intra_kind(kind a)"
  shows "valid_path_rev_aux cs as ⟹ valid_path_rev_aux cs (a#as)"
proof(induct rule:vpra_induct)
  case (vpra_empty cs)
  have "valid_path_rev_aux cs []" by simp
  with ‹intra_kind(kind a)› have "valid_path_rev_aux cs ([]@[a])"
    by(simp only:valid_path_rev_aux.simps intra_kind_def,fastforce)
  thus ?case by simp
qed(simp only:append_Cons[THEN sym] valid_path_rev_aux.simps intra_kind_def,fastforce)+


lemma vpra_Cons_Return:
  assumes "kind a = Q↩⇘p⇙f"
  shows "valid_path_rev_aux cs as ⟹ valid_path_rev_aux cs (a#as)"
proof(induct rule:vpra_induct)
  case (vpra_empty cs)
  from ‹kind a = Q↩⇘p⇙f› have "valid_path_rev_aux cs ([]@[a])"
    by(simp only:valid_path_rev_aux.simps,clarsimp)
  thus ?case by simp
next
  case (vpra_intra cs a' as')
  from ‹valid_path_rev_aux cs (a#as')› ‹intra_kind (kind a')›
  have "valid_path_rev_aux cs ((a#as')@[a'])"
    by(simp only:valid_path_rev_aux.simps,fastforce simp:intra_kind_def)
  thus ?case by simp
next
  case (vpra_Return cs a' as' Q' p' f')
  from ‹valid_path_rev_aux (a'#cs) (a#as')› ‹kind a' = Q'↩⇘p'⇙f'›
  have "valid_path_rev_aux cs ((a#as')@[a'])"
    by(simp only:valid_path_rev_aux.simps,clarsimp)
  thus ?case by simp
next
  case (vpra_CallEmpty cs a' as' Q' r' p' fs')
  from ‹valid_path_rev_aux [] (a#as')› ‹kind a' = Q':r'↪⇘p'⇙fs'› ‹cs = []›
  have "valid_path_rev_aux cs ((a#as')@[a'])"
    by(simp only:valid_path_rev_aux.simps,clarsimp)
  thus ?case by simp
next
  case (vpra_CallCons cs a' as' Q' r' p' fs' c' cs')
  from ‹valid_path_rev_aux cs' (a#as')› ‹kind a' = Q':r'↪⇘p'⇙fs'› ‹cs = c'#cs'›
    ‹c' ∈ get_return_edges a'›
  have "valid_path_rev_aux cs ((a#as')@[a'])"
    by(simp only:valid_path_rev_aux.simps,clarsimp)
  thus ?case by simp
qed


(*<*)
lemmas append_Cons_rev = append_Cons[THEN sym]
declare append_Cons [simp del] append_Cons_rev [simp]
(*>*)

lemma upd_rev_cs_Cons_intra:
  assumes "intra_kind(kind a)" shows "upd_rev_cs cs (a#as) = upd_rev_cs cs as"
proof(induct as arbitrary:cs rule:rev_induct)
  case Nil
  from ‹intra_kind (kind a)›
  have "upd_rev_cs cs ([]@[a]) = upd_rev_cs cs []"
    by(simp only:upd_rev_cs.simps,auto simp:intra_kind_def)
  thus ?case by simp
next
  case (snoc a' as')
  note IH = ‹⋀cs. upd_rev_cs cs (a#as') = upd_rev_cs cs as'›
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    from IH have "upd_rev_cs cs (a#as') = upd_rev_cs cs as'" .
    with Intra have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
      by(fastforce simp:intra_kind_def)
    thus ?thesis by simp
  next
    case Return
    from IH have "upd_rev_cs (a'#cs) (a#as') = upd_rev_cs (a'#cs) as'" .
    with Return have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
      by(auto simp:intra_kind_def)
    thus ?thesis by simp
  next
    case Call
    show ?thesis
    proof(cases cs)
      case Nil
      from IH have "upd_rev_cs [] (a#as') = upd_rev_cs [] as'" .
      with Call Nil have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
        by(auto simp:intra_kind_def)
      thus ?thesis by simp
    next
      case (Cons c' cs')
      from IH have "upd_rev_cs cs' (a#as') = upd_rev_cs cs' as'" .
      with Call Cons have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
        by(auto simp:intra_kind_def)
      thus ?thesis by simp
    qed
  qed
qed



lemma upd_rev_cs_Cons_Return:
  assumes "kind a = Q↩⇘p⇙f" shows "upd_rev_cs cs (a#as) = a#(upd_rev_cs cs as)"
proof(induct as arbitrary:cs rule:rev_induct)
  case Nil
  with ‹kind a = Q↩⇘p⇙f› have "upd_rev_cs cs ([]@[a]) = a#(upd_rev_cs cs [])"
    by(simp only:upd_rev_cs.simps) clarsimp
  thus ?case by simp
next
  case (snoc a' as')
  note IH = ‹⋀cs. upd_rev_cs cs (a#as') = a#upd_rev_cs cs as'›
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    from IH have "upd_rev_cs cs (a#as') = a#(upd_rev_cs cs as')" .
    with Intra have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
      by(fastforce simp:intra_kind_def)
    thus ?thesis by simp
  next
    case Return
    from IH have "upd_rev_cs (a'#cs) (a#as') = a#(upd_rev_cs (a'#cs) as')" .
    with Return have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
      by(auto simp:intra_kind_def)
    thus ?thesis by simp
  next
    case Call
    show ?thesis
    proof(cases cs)
      case Nil
      from IH have "upd_rev_cs [] (a#as') = a#(upd_rev_cs [] as')" .
      with Call Nil have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
        by(auto simp:intra_kind_def)
      thus ?thesis by simp
    next
      case (Cons c' cs')
      from IH have "upd_rev_cs cs' (a#as') = a#(upd_rev_cs cs' as')" .
      with Call Cons 
      have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
        by(auto simp:intra_kind_def)
      thus ?thesis by simp
    qed
  qed
qed


lemma upd_rev_cs_Cons_Call_Cons:
  assumes "kind a = Q:r↪⇘p⇙fs"
  shows "upd_rev_cs cs as = c'#cs' ⟹ upd_rev_cs cs (a#as) = cs'"
proof(induct as arbitrary:cs rule:rev_induct)
  case Nil
  with ‹kind a = Q:r↪⇘p⇙fs› have "upd_rev_cs cs ([]@[a]) = cs'"
    by(simp only:upd_rev_cs.simps) clarsimp
 thus ?case by simp
next
  case (snoc a' as')
  note IH = ‹⋀cs. upd_rev_cs cs as' = c'#cs' ⟹ upd_rev_cs cs (a#as') = cs'›
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    with ‹upd_rev_cs cs (as'@[a']) = c'#cs'›
    have "upd_rev_cs cs as' = c'#cs'" by(fastforce simp:intra_kind_def)
    from IH[OF this] have "upd_rev_cs cs (a#as') = cs'" .
    with Intra show ?thesis by(fastforce simp:intra_kind_def)
  next
    case Return
    with ‹upd_rev_cs cs (as'@[a']) = c'#cs'›
    have "upd_rev_cs (a'#cs) as' = c'#cs'" by simp
    from IH[OF this] have "upd_rev_cs (a'#cs) (a#as') = cs'" .
    with Return show ?thesis by simp
  next
    case Call
    show ?thesis
    proof(cases cs)
      case Nil
      with ‹upd_rev_cs cs (as'@[a']) = c'#cs'› Call
      have "upd_rev_cs cs as' = c'#cs'" by simp
      from IH[OF this] have "upd_rev_cs cs (a#as') = cs'" .
      with Nil Call show ?thesis by simp
    next
      case (Cons cx csx)
      with ‹upd_rev_cs cs (as'@[a']) = c'#cs'› Call
      have "upd_rev_cs csx as' = c'#cs'" by simp
      from IH[OF this] have "upd_rev_cs csx (a#as') = cs'" .
      with Cons Call show ?thesis by simp
    qed
  qed
qed


lemma upd_rev_cs_Cons_Call_Cons_Empty:
  assumes "kind a = Q:r↪⇘p⇙fs"
  shows "upd_rev_cs cs as = [] ⟹ upd_rev_cs cs (a#as) = []"
proof(induct as arbitrary:cs rule:rev_induct)
  case Nil
  with ‹kind a = Q:r↪⇘p⇙fs› have "upd_rev_cs cs ([]@[a]) = []"
    by(simp only:upd_rev_cs.simps) clarsimp
 thus ?case by simp
next
  case (snoc a' as')
  note IH = ‹⋀cs. upd_rev_cs cs as' = [] ⟹ upd_rev_cs cs (a#as') = []›
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    with ‹upd_rev_cs cs (as'@[a']) = []›
    have "upd_rev_cs cs as' = []" by(fastforce simp:intra_kind_def)
    from IH[OF this] have "upd_rev_cs cs (a#as') = []" .
    with Intra show ?thesis by(fastforce simp:intra_kind_def)
  next
    case Return
    with ‹upd_rev_cs cs (as'@[a']) = []›
    have "upd_rev_cs (a'#cs) as' = []" by simp
    from IH[OF this] have "upd_rev_cs (a'#cs) (a#as') = []" .
    with Return show ?thesis by simp
  next
    case Call
    show ?thesis
    proof(cases cs)
      case Nil
      with ‹upd_rev_cs cs (as'@[a']) = []› Call
      have "upd_rev_cs cs as' = []" by simp
      from IH[OF this] have "upd_rev_cs cs (a#as') = []" .
      with Nil Call show ?thesis by simp
    next
      case (Cons cx csx)
      with ‹upd_rev_cs cs (as'@[a']) = []› Call
      have "upd_rev_cs csx as' = []" by simp
      from IH[OF this] have "upd_rev_cs csx (a#as') = []" .
      with Cons Call show ?thesis by simp
    qed
  qed
qed

(*<*)declare append_Cons [simp] append_Cons_rev [simp del](*>*)


definition valid_call_list :: "'edge list ⇒ 'node ⇒ bool"
  where "valid_call_list cs n ≡
  ∀cs' c cs''. cs = cs'@c#cs'' ⟶ (valid_edge c ∧ (∃Q r p fs. (kind c = Q:r↪⇘p⇙fs) ∧ 
                    p = get_proc (case cs' of [] ⇒ n | _ ⇒ last (sourcenodes cs'))))"

definition valid_return_list :: "'edge list ⇒ 'node ⇒ bool"
  where "valid_return_list cs n ≡
  ∀cs' c cs''. cs = cs'@c#cs'' ⟶ (valid_edge c ∧ (∃Q p f. (kind c = Q↩⇘p⇙f) ∧ 
                    p = get_proc (case cs' of [] ⇒ n | _ ⇒ last (targetnodes cs'))))"


lemma valid_call_list_valid_edges: 
  assumes "valid_call_list cs n" shows "∀c ∈ set cs. valid_edge c"
proof -
  from ‹valid_call_list cs n› 
  have "∀cs' c cs''. cs = cs'@c#cs'' ⟶ valid_edge c"
    by(simp add:valid_call_list_def)
  thus ?thesis
  proof(induct cs)
    case Nil thus ?case by simp
  next
    case (Cons cx csx)
    note IH = ‹∀cs' c cs''. csx = cs'@c#cs'' ⟶ valid_edge c ⟹
                            ∀a∈set csx. valid_edge a›
    from ‹∀cs' c cs''. cx#csx = cs'@c#cs'' ⟶ valid_edge c›
    have "valid_edge cx" by blast
    from ‹∀cs' c cs''. cx#csx = cs'@c#cs'' ⟶ valid_edge c›
    have "∀cs' c cs''. csx = cs'@c#cs'' ⟶ valid_edge c"
      by auto(erule_tac x="cx#cs'" in allE,auto)
    from IH[OF this] ‹valid_edge cx› show ?case by simp
  qed
qed


lemma valid_return_list_valid_edges: 
  assumes "valid_return_list rs n" shows "∀r ∈ set rs. valid_edge r"
proof -
  from ‹valid_return_list rs n› 
  have "∀rs' r rs''. rs = rs'@r#rs'' ⟶ valid_edge r"
    by(simp add:valid_return_list_def)
  thus ?thesis
  proof(induct rs)
    case Nil thus ?case by simp
  next
    case (Cons rx rsx)
    note IH = ‹∀rs' r rs''. rsx = rs'@r#rs'' ⟶ valid_edge r ⟹
                            ∀a∈set rsx. valid_edge a›
    from ‹∀rs' r rs''. rx#rsx = rs'@r#rs'' ⟶ valid_edge r›
    have "valid_edge rx" by blast
    from ‹∀rs' r rs''. rx#rsx = rs'@r#rs'' ⟶ valid_edge r›
    have "∀rs' r rs''. rsx = rs'@r#rs'' ⟶ valid_edge r"
      by auto(erule_tac x="rx#rs'" in allE,auto)
    from IH[OF this] ‹valid_edge rx› show ?case by simp
  qed
qed


lemma vpra_empty_valid_call_list_rev:
  "valid_call_list cs n ⟹ valid_path_rev_aux [] (rev cs)"
proof(induct cs arbitrary:n)
  case Nil thus ?case by simp
next
  case (Cons c' cs')
  note IH = ‹⋀n. valid_call_list cs' n ⟹ valid_path_rev_aux [] (rev cs')›
  from ‹valid_call_list (c'#cs') n› have "valid_call_list cs' (sourcenode c')"
    apply(clarsimp simp:valid_call_list_def)
    apply hypsubst_thin
    apply(erule_tac x="c'#cs'" in allE)
    apply clarsimp
    by(case_tac cs',auto simp:sourcenodes_def)
  from IH[OF this] have "valid_path_rev_aux [] (rev cs')" .
  moreover
  from ‹valid_call_list (c'#cs') n› obtain Q r p fs where "kind c' = Q:r↪⇘p⇙fs"
    apply(clarsimp simp:valid_call_list_def)
    by(erule_tac x="[]" in allE) fastforce
  ultimately show ?case by simp
qed


lemma vpa_upd_cs_cases:
  "⟦valid_path_aux cs as; valid_call_list cs n; n -as→* n'⟧
  ⟹ case (upd_cs cs as) of [] ⇒ (∀c ∈ set cs. ∃a ∈ set as. a ∈ get_return_edges c)
                      | cx#csx ⇒ valid_call_list (cx#csx) n'"
proof(induct arbitrary:n rule:vpa_induct)
  case (vpa_empty cs)
  from ‹n -[]→* n'› have "n = n'" by fastforce
  with ‹valid_call_list cs n› show ?case by(cases cs) auto
next
  case (vpa_intra cs a' as')
  note IH = ‹⋀n. ⟦valid_call_list cs n; n -as'→* n'⟧
    ⟹ case (upd_cs cs as') of [] ⇒ ∀c∈set cs. ∃a∈set as'. a ∈ get_return_edges c
                         | cx#csx ⇒ valid_call_list (cx # csx) n'›
  from ‹intra_kind (kind a')› have "upd_cs cs (a'#as') = upd_cs cs as'"
    by(fastforce simp:intra_kind_def)
  from ‹n -a'#as'→* n'› have [simp]:"n = sourcenode a'" and "valid_edge a'"
    and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
  from ‹valid_edge a'› ‹intra_kind (kind a')›
  have "get_proc (sourcenode a') = get_proc (targetnode a')" by(rule get_proc_intra)
  with ‹valid_call_list cs n› have "valid_call_list cs (targetnode a')"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="cs'" in allE) apply clarsimp
    by(case_tac cs') auto
  from IH[OF this ‹targetnode a' -as'→* n'›] ‹upd_cs cs (a'#as') = upd_cs cs as'›
  show ?case by(cases "upd_cs cs as'") auto
next
  case (vpa_Call cs a' as' Q r p fs)
  note IH = ‹⋀n. ⟦valid_call_list (a'#cs) n; n -as'→* n'⟧
    ⟹ case (upd_cs (a'#cs) as') 
             of [] ⇒ ∀c∈set (a'#cs). ∃a∈set as'. a ∈ get_return_edges c
          | cx#csx ⇒ valid_call_list (cx # csx) n'›
  from ‹kind a' = Q:r↪⇘p⇙fs› have "upd_cs (a'#cs) as' = upd_cs cs (a'#as')"
    by simp
  from ‹n -a'#as'→* n'› have [simp]:"n = sourcenode a'" and "valid_edge a'"
    and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
  from ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs›
  have "get_proc (targetnode a') = p" by(rule get_proc_call)
  with ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs› ‹valid_call_list cs n›
  have "valid_call_list (a'#cs) (targetnode a')"
    apply(clarsimp simp:valid_call_list_def)
    apply(case_tac cs') apply auto
    apply(erule_tac x="list" in allE) apply clarsimp
    by(case_tac list,auto simp:sourcenodes_def)
  from IH[OF this ‹targetnode a' -as'→* n'›] 
    ‹upd_cs (a'#cs) as' = upd_cs cs (a'#as')›
  have "case upd_cs cs (a'#as') 
         of [] ⇒ ∀c∈set (a' # cs). ∃a∈set as'. a ∈ get_return_edges c
    | cx # csx ⇒ valid_call_list (cx # csx) n'" by simp
  thus ?case by(cases "upd_cs cs (a'#as')") simp+
next
  case (vpa_ReturnEmpty cs a' as' Q p f)
  note IH = ‹⋀n. ⟦valid_call_list [] n; n -as'→* n'⟧
    ⟹ case (upd_cs [] as') 
             of [] ⇒ ∀c∈set []. ∃a∈set as'. a ∈ get_return_edges c
          | cx#csx ⇒ valid_call_list (cx # csx) n'›
  from ‹kind a' = Q↩⇘p⇙f› ‹cs = []› have "upd_cs [] as' = upd_cs cs (a'#as')"
    by simp
  from ‹n -a'#as'→* n'› have [simp]:"n = sourcenode a'" and "valid_edge a'"
    and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
  have "valid_call_list [] (targetnode a')" by(simp add:valid_call_list_def)
  from IH[OF this ‹targetnode a' -as'→* n'›]
    ‹upd_cs [] as' = upd_cs cs (a'#as')›
  have "case (upd_cs cs (a'#as')) 
         of [] ⇒ ∀c∈set []. ∃a∈set as'. a ∈ get_return_edges c
    | cx#csx ⇒ valid_call_list (cx#csx) n'" by simp
  with ‹cs = []› show ?case by(cases "upd_cs cs (a'#as')") simp+
next
  case (vpa_ReturnCons cs a' as' Q p f c' cs')
  note IH = ‹⋀n. ⟦valid_call_list cs' n; n -as'→* n'⟧
    ⟹ case (upd_cs cs' as') 
             of [] ⇒ ∀c∈set cs'. ∃a∈set as'. a ∈ get_return_edges c
          | cx#csx ⇒ valid_call_list (cx # csx) n'›
  from ‹kind a' = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a' ∈ get_return_edges c'› 
  have "upd_cs cs' as' = upd_cs cs (a'#as')" by simp
  from ‹n -a'#as'→* n'› have [simp]:"n = sourcenode a'" and "valid_edge a'"
    and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
  from ‹valid_call_list cs n› ‹cs = c'#cs'› have "valid_edge c'"
    apply(clarsimp simp:valid_call_list_def)
    by(erule_tac x="[]" in allE,auto)
  with ‹a' ∈ get_return_edges c'› obtain ax where "valid_edge ax"
    and sources:"sourcenode ax = sourcenode c'" 
    and targets:"targetnode ax = targetnode a'" and "kind ax = (λcf. False)⇩√"
    by(fastforce dest:call_return_node_edge)
  from ‹valid_edge ax› sources[THEN sym] targets[THEN sym] ‹kind ax = (λcf. False)⇩√›
  have "get_proc (sourcenode c') = get_proc (targetnode a')"
    by(fastforce intro:get_proc_intra simp:intra_kind_def)
  with ‹valid_call_list cs n› ‹cs = c'#cs'›
  have "valid_call_list cs' (targetnode a')"
    apply(clarsimp simp:valid_call_list_def)
    apply(hypsubst_thin)
    apply(erule_tac x="c'#cs'" in allE)
    by(case_tac cs',auto simp:sourcenodes_def)
  from IH[OF this ‹targetnode a' -as'→* n'›] 
    ‹upd_cs cs' as' = upd_cs cs (a'#as')›
  have "case (upd_cs cs (a'#as')) 
         of [] ⇒ ∀c∈set cs'. ∃a∈set as'. a ∈ get_return_edges c
    | cx#csx ⇒ valid_call_list (cx#csx) n'" by simp
  with ‹cs = c' # cs'› ‹a' ∈ get_return_edges c'› show ?case
    by(cases "upd_cs cs (a'#as')") simp+
qed


lemma vpa_valid_call_list_valid_return_list_vpra:
  "⟦valid_path_aux cs cs'; valid_call_list cs n; valid_return_list cs' n'⟧
  ⟹ valid_path_rev_aux cs' (rev cs)"
proof(induct arbitrary:n n' rule:vpa_induct)
  case (vpa_empty cs)
  from ‹valid_call_list cs n› show ?case by(rule vpra_empty_valid_call_list_rev)
next
  case (vpa_intra cs a as)
  from ‹intra_kind (kind a)› ‹valid_return_list (a#as) n'›
  have False apply(clarsimp simp:valid_return_list_def)
    by(erule_tac x="[]" in allE,clarsimp simp:intra_kind_def)
  thus ?case by simp
next
  case (vpa_Call cs a as Q r p fs)
  from ‹kind a = Q:r↪⇘p⇙fs› ‹valid_return_list (a#as) n'›
  have False apply(clarsimp simp:valid_return_list_def)
    by(erule_tac x="[]" in allE,clarsimp)
  thus ?case by simp
next
  case (vpa_ReturnEmpty cs a as Q p f)
  from ‹cs = []› show ?case by simp
next
  case (vpa_ReturnCons cs a as Q p f c' cs')
  note IH = ‹⋀n n'. ⟦valid_call_list cs' n; valid_return_list as n'⟧
    ⟹ valid_path_rev_aux as (rev cs')›
  from ‹valid_return_list (a#as) n'› have "valid_return_list as (targetnode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="a#cs'" in allE)
    by(case_tac cs',auto simp:targetnodes_def)
  from ‹valid_call_list cs n› ‹cs = c'#cs'›
  have "valid_call_list cs' (sourcenode c')"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="c'#cs'" in allE)
    by(case_tac cs',auto simp:sourcenodes_def)
  from ‹valid_call_list cs n› ‹cs = c'#cs'› have "valid_edge c'"
    apply(clarsimp simp:valid_call_list_def)
    by(erule_tac x="[]" in allE,auto)
  with ‹a ∈ get_return_edges c'› obtain Q' r' p' f' where "kind c' = Q':r'↪⇘p'⇙f'"
    apply(cases "kind c'" rule:edge_kind_cases)
    by(auto dest:only_call_get_return_edges simp:intra_kind_def)
  from IH[OF ‹valid_call_list cs' (sourcenode c')›
    ‹valid_return_list as (targetnode a)›]
  have "valid_path_rev_aux as (rev cs')" .
  with ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› ‹kind c' = Q':r'↪⇘p'⇙f'›
  show ?case by simp
qed
 


lemma vpa_to_vpra:
  "⟦valid_path_aux cs as; valid_path_aux (upd_cs cs as) cs'; 
    n -as→* n'; valid_call_list cs n; valid_return_list cs' n''⟧ 
  ⟹ valid_path_rev_aux cs' as ∧ valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)"
proof(induct arbitrary:n rule:vpa_induct)
  case vpa_empty thus ?case
    by(fastforce intro:vpa_valid_call_list_valid_return_list_vpra)
next
  case (vpa_intra cs a as)
  note IH = ‹⋀n. ⟦valid_path_aux (upd_cs cs as) cs'; n -as→* n';
    valid_call_list cs n; valid_return_list cs' n''⟧
    ⟹ valid_path_rev_aux cs' as ∧
       valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)›
  from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
  from ‹valid_edge a› ‹intra_kind (kind a)›
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  with ‹valid_call_list cs n› ‹n = sourcenode a›
  have "valid_call_list cs (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="cs'" in allE) apply clarsimp
    by(case_tac cs') auto
  from ‹valid_path_aux (upd_cs cs (a#as)) cs'› ‹intra_kind (kind a)›
  have "valid_path_aux (upd_cs cs as) cs'"
    by(fastforce simp:intra_kind_def)
  from IH[OF this ‹targetnode a -as→* n'› ‹valid_call_list cs (targetnode a)›
    ‹valid_return_list cs' n''›]
  have "valid_path_rev_aux cs' as" 
    and "valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)" by simp_all
  from  ‹intra_kind (kind a)› ‹valid_path_rev_aux cs' as›
  have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_intra)
  from ‹intra_kind (kind a)› have "upd_rev_cs cs' (a#as) = upd_rev_cs cs' as"
    by(simp add:upd_rev_cs_Cons_intra)
  with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)›
  have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
  with ‹valid_path_rev_aux cs' (a#as)› show ?case by simp
next
  case (vpa_Call cs a as Q r p fs)
  note IH = ‹⋀n. ⟦valid_path_aux (upd_cs (a#cs) as) cs'; n -as→* n';
    valid_call_list (a#cs) n; valid_return_list cs' n''⟧
    ⟹ valid_path_rev_aux cs' as ∧
       valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))›
  from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "p = get_proc (targetnode a)"
    by(rule get_proc_call[THEN sym])
  from ‹valid_call_list cs n› ‹n = sourcenode a›
  have "valid_call_list cs (sourcenode a)" by simp
  with ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge a› ‹p = get_proc (targetnode a)›
  have "valid_call_list (a#cs) (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(case_tac cs') apply auto
    apply(erule_tac x="list" in allE) apply clarsimp
    by(case_tac list,auto simp:sourcenodes_def)
  from ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs cs (a#as) = upd_cs (a#cs) as"
    by simp
  with ‹valid_path_aux (upd_cs cs (a#as)) cs'›
  have "valid_path_aux (upd_cs (a#cs) as) cs'" by simp
  from IH[OF this ‹targetnode a -as→* n'› ‹valid_call_list (a#cs) (targetnode a)›
    ‹valid_return_list cs' n''›]
  have "valid_path_rev_aux cs' as"
    and "valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))" by simp_all
  show ?case
  proof(cases "upd_rev_cs cs' as")
    case Nil
    with ‹kind a = Q:r↪⇘p⇙fs›
    have "upd_rev_cs cs' (a#as) = []" by(rule upd_rev_cs_Cons_Call_Cons_Empty)
    with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))› ‹kind a = Q:r↪⇘p⇙fs› Nil
    have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
    from Nil ‹kind a = Q:r↪⇘p⇙fs› have "valid_path_rev_aux (upd_rev_cs cs' as) ([]@[a])"
      by(simp only:valid_path_rev_aux.simps) clarsimp
    with ‹valid_path_rev_aux cs' as› have "valid_path_rev_aux cs' ([a]@as)"
      by(fastforce intro:valid_path_rev_aux_Append)
    with ‹valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)›
    show ?thesis by simp
  next
    case (Cons cx csx)
    with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))› ‹kind a = Q:r↪⇘p⇙fs›
    have match:"cx ∈ get_return_edges a" "valid_path_rev_aux csx (rev cs)" by auto
    from ‹kind a = Q:r↪⇘p⇙fs› Cons have "upd_rev_cs cs' (a#as) = csx"
      by(rule upd_rev_cs_Cons_Call_Cons)
    with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev(a#cs))› ‹kind a = Q:r↪⇘p⇙fs› match
    have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
    from Cons ‹kind a = Q:r↪⇘p⇙fs› match
    have "valid_path_rev_aux (upd_rev_cs cs' as) ([]@[a])"
      by(simp only:valid_path_rev_aux.simps) clarsimp
    with ‹valid_path_rev_aux cs' as› have "valid_path_rev_aux cs' ([a]@as)"
      by(fastforce intro:valid_path_rev_aux_Append)
    with ‹valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)›
    show ?thesis by simp
  qed
next
  case (vpa_ReturnEmpty cs a as Q p f)
  note IH = ‹⋀n. ⟦valid_path_aux (upd_cs [] as) cs'; n -as→* n';
    valid_call_list [] n; valid_return_list cs' n''⟧
    ⟹ valid_path_rev_aux cs' as ∧
       valid_path_rev_aux (upd_rev_cs cs' as) (rev [])›
  from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
  from ‹cs = []› ‹kind a = Q↩⇘p⇙f› have "upd_cs cs (a#as) = upd_cs [] as"
    by simp
  with ‹valid_path_aux (upd_cs cs (a#as)) cs'›
  have "valid_path_aux (upd_cs [] as) cs'" by simp
  from IH[OF this ‹targetnode a -as→* n'› _ ‹valid_return_list cs' n''›]
  have "valid_path_rev_aux cs' as" 
    and "valid_path_rev_aux (upd_rev_cs cs' as) (rev [])" 
    by(auto simp:valid_call_list_def)
  from ‹kind a = Q↩⇘p⇙f› ‹valid_path_rev_aux cs' as›
  have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_Return)
  moreover
  from ‹cs = []› have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)"
    by simp
  ultimately show ?case by simp
next
  case (vpa_ReturnCons cs a as Q p f cx csx)
  note IH = ‹⋀n. ⟦valid_path_aux (upd_cs csx as) cs'; n -as→* n';
    valid_call_list csx n; valid_return_list cs' n''⟧
    ⟹ valid_path_rev_aux cs' as ∧
       valid_path_rev_aux (upd_rev_cs cs' as) (rev csx)›
  note match = ‹cs = cx#csx› ‹a ∈ get_return_edges cx›
  from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
  from ‹cs = cx#csx› ‹valid_call_list cs n› have "valid_edge cx"
    apply(clarsimp simp:valid_call_list_def)
    by(erule_tac x="[]" in allE) clarsimp
  with match have "get_proc (sourcenode cx) = get_proc (targetnode a)"
    by(fastforce intro:get_proc_get_return_edge)
  with ‹valid_call_list cs n› ‹cs = cx#csx›
  have "valid_call_list csx (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="cx#cs'" in allE) apply clarsimp
    by(case_tac cs',auto simp:sourcenodes_def)
  from ‹kind a = Q↩⇘p⇙f› match have "upd_cs cs (a#as) = upd_cs csx as" by simp
  with ‹valid_path_aux (upd_cs cs (a#as)) cs'›
  have "valid_path_aux (upd_cs csx as) cs'" by simp
  from IH[OF this ‹targetnode a -as→* n'› ‹valid_call_list csx (targetnode a)›
    ‹valid_return_list cs' n''›]
  have "valid_path_rev_aux cs' as" 
    and "valid_path_rev_aux (upd_rev_cs cs' as) (rev csx)" by simp_all
  from ‹kind a = Q↩⇘p⇙f› ‹valid_path_rev_aux cs' as›
  have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_Return)
  from match ‹valid_edge cx› obtain Q' r' p' f' where "kind cx = Q':r'↪⇘p'⇙f'"
    by(fastforce dest!:only_call_get_return_edges)
  from ‹kind a = Q↩⇘p⇙f› have "upd_rev_cs cs' (a#as) = a#(upd_rev_cs cs' as)"
    by(rule upd_rev_cs_Cons_Return)
  with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev csx)› ‹kind a = Q↩⇘p⇙f› 
    ‹kind cx = Q':r'↪⇘p'⇙f'› match
  have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)"
    by simp
  with ‹valid_path_rev_aux cs' (a#as)› show ?case by simp
qed


lemma vp_to_vpra:
  "n -as→⇩√* n' ⟹ valid_path_rev_aux [] as"
by(fastforce elim:vpa_to_vpra[THEN conjunct1] 
            simp:vp_def valid_path_def valid_call_list_def valid_return_list_def)




subsubsection ‹Same level paths›


fun same_level_path_aux :: "'edge list ⇒ 'edge list ⇒ bool"
  where "same_level_path_aux cs [] ⟷ True"
  | "same_level_path_aux cs (a#as) ⟷ 
       (case (kind a) of Q:r↪⇘p⇙fs ⇒ same_level_path_aux (a#cs) as
                       | Q↩⇘p⇙f ⇒ case cs of [] ⇒ False
                                     | c'#cs' ⇒ a ∈ get_return_edges c' ∧
                                             same_level_path_aux cs' as
                       |    _ ⇒ same_level_path_aux cs as)"


lemma slpa_induct [consumes 1,case_names slpa_empty slpa_intra slpa_Call 
  slpa_Return]:
  assumes major: "same_level_path_aux xs ys"
  and rules: "⋀cs. P cs []"
    "⋀cs a as. ⟦intra_kind(kind a); same_level_path_aux cs as; P cs as⟧ 
      ⟹ P cs (a#as)"
    "⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; same_level_path_aux (a#cs) as; P (a#cs) as⟧ 
      ⟹ P cs (a#as)"
    "⋀cs a as Q p f c' cs'. ⟦kind a = Q↩⇘p⇙f; cs = c'#cs'; same_level_path_aux cs' as;
                             a ∈ get_return_edges c'; P cs' as⟧
     ⟹ P cs (a#as)"
  shows "P xs ys"
using major
apply(induct ys arbitrary: xs)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)


lemma slpa_cases [consumes 4,case_names intra_path return_intra_path]:
  assumes "same_level_path_aux cs as" and "upd_cs cs as = []"
  and "∀c ∈ set cs. valid_edge c" and "∀a ∈ set as. valid_edge a"
  obtains "∀a ∈ set as. intra_kind(kind a)"
  | asx a asx' Q p f c' cs' where "as = asx@a#asx'" and "same_level_path_aux cs asx"
    and "kind a = Q↩⇘p⇙f" and "upd_cs cs asx = c'#cs'" and "upd_cs cs (asx@[a]) = []" 
    and "a ∈ get_return_edges c'" and "valid_edge c'"
    and "∀a ∈ set asx'. intra_kind(kind a)"
proof(atomize_elim)
  from assms
  show "(∀a∈set as. intra_kind (kind a)) ∨
    (∃asx a asx' Q p f c' cs'. as = asx@a#asx' ∧ same_level_path_aux cs asx ∧
       kind a = Q↩⇘p⇙f ∧ upd_cs cs asx = c'#cs' ∧ upd_cs cs (asx@[a]) = [] ∧ 
       a ∈ get_return_edges c' ∧ valid_edge c' ∧ (∀a∈set asx'. intra_kind (kind a)))"
  proof(induct rule:slpa_induct)
    case (slpa_empty cs)
    have "∀a∈set []. intra_kind (kind a)" by simp
    thus ?case by simp
  next
    case (slpa_intra cs a as)
    note IH = ‹⟦upd_cs cs as = []; ∀c∈set cs. valid_edge c; ∀a'∈set as. valid_edge a'⟧ 
      ⟹ (∀a∈set as. intra_kind (kind a)) ∨
      (∃asx a asx' Q p f c' cs'. as = asx@a#asx' ∧ same_level_path_aux cs asx ∧
        kind a = Q↩⇘p⇙f ∧  upd_cs cs asx = c' # cs' ∧ upd_cs cs (asx@[a]) = [] ∧ 
        a ∈ get_return_edges c' ∧ valid_edge c' ∧ (∀a∈set asx'. intra_kind (kind a)))›
    from ‹∀a'∈set (a#as). valid_edge a'› have "∀a'∈set as. valid_edge a'" by simp
    from ‹intra_kind (kind a)› ‹upd_cs cs (a#as) = []›
    have "upd_cs cs as = []" by(fastforce simp:intra_kind_def)
    from IH[OF this ‹∀c∈set cs. valid_edge c› ‹∀a'∈set as. valid_edge a'›] show ?case
    proof
      assume "∀a∈set as. intra_kind (kind a)"
      with ‹intra_kind (kind a)› have "∀a'∈set (a#as). intra_kind (kind a')"
        by simp
      thus ?case by simp
    next
      assume "∃asx a asx' Q p f c' cs'. as = asx@a#asx' ∧ same_level_path_aux cs asx ∧
                kind a = Q↩⇘p⇙f ∧ upd_cs cs asx = c'#cs' ∧ upd_cs cs (asx@[a]) = [] ∧ 
                a ∈ get_return_edges c' ∧ valid_edge c' ∧ 
                (∀a∈set asx'. intra_kind (kind a))"
      then obtain asx a' Q p f asx' c' cs' where "as = asx@a'#asx'" 
        and "same_level_path_aux cs asx" and "upd_cs cs (asx@[a']) = []"
        and "upd_cs cs asx = c'#cs'" and assms:"a' ∈ get_return_edges c'"
        "kind a' = Q↩⇘p⇙f" "valid_edge c'" "∀a∈set asx'. intra_kind (kind a)"
        by blast
      from ‹as = asx@a'#asx'› have "a#as = (a#asx)@a'#asx'" by simp
      moreover
      from ‹intra_kind (kind a)› ‹same_level_path_aux cs asx›
      have "same_level_path_aux cs (a#asx)" by(fastforce simp:intra_kind_def)
      moreover
      from ‹upd_cs cs asx = c'#cs'› ‹intra_kind (kind a)›
      have "upd_cs cs (a#asx) = c'#cs'" by(fastforce simp:intra_kind_def)
      moreover
      from ‹upd_cs cs (asx@[a']) = []› ‹intra_kind (kind a)›
      have "upd_cs cs ((a#asx)@[a']) = []" by(fastforce simp:intra_kind_def)
      ultimately show ?case using assms by blast
    qed
  next
    case (slpa_Call cs a as Q r p fs)
    note IH = ‹⟦upd_cs (a#cs) as = []; ∀c∈set (a#cs). valid_edge c;
      ∀a'∈set as. valid_edge a'⟧ ⟹ 
      (∀a'∈set as. intra_kind (kind a')) ∨
      (∃asx a' asx' Q' p' f' c' cs'. as = asx@a'#asx' ∧ 
        same_level_path_aux (a#cs) asx ∧ kind a' = Q'↩⇘p'⇙f' ∧ 
        upd_cs (a#cs) asx = c'#cs' ∧ upd_cs (a#cs) (asx@[a']) = [] ∧ 
        a' ∈ get_return_edges c' ∧ valid_edge c' ∧ 
        (∀a'∈set asx'. intra_kind (kind a')))›
    from ‹∀a'∈set (a#as). valid_edge a'› have "valid_edge a" 
      and "∀a'∈set as. valid_edge a'" by simp_all
    from ‹∀c∈set cs. valid_edge c› ‹valid_edge a› have "∀c∈set (a#cs). valid_edge c"
      by simp
    from ‹upd_cs cs (a#as) = []› ‹kind a = Q:r↪⇘p⇙fs›
    have "upd_cs (a#cs) as = []" by simp
    from IH[OF this ‹∀c∈set (a#cs). valid_edge c› ‹∀a'∈set as. valid_edge a'›]
    show ?case
    proof
      assume "∀a'∈set as. intra_kind (kind a')"
      with ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs cs (a#as) = a#cs"
        by(fastforce intro:upd_cs_intra_path)
      with ‹upd_cs cs (a#as) = []› have False by simp
      thus ?case by simp
    next
      assume "∃asx a' asx' Q p f c' cs'. as = asx@a'#asx' ∧ 
                same_level_path_aux (a#cs) asx ∧ kind a' = Q↩⇘p⇙f ∧ 
                upd_cs (a#cs) asx = c'#cs' ∧ upd_cs (a#cs) (asx@[a']) = [] ∧ 
                a' ∈ get_return_edges c' ∧ valid_edge c' ∧ 
                (∀a∈set asx'. intra_kind (kind a))"
      then obtain asx a' Q' p' f' asx' c' cs' where "as = asx@a'#asx'" 
        and "same_level_path_aux (a#cs) asx" and "upd_cs (a#cs) (asx@[a']) = []"
        and "upd_cs (a#cs) asx = c'#cs'" and assms:"a' ∈ get_return_edges c'"
        "kind a' = Q'↩⇘p'⇙f'" "valid_edge c'" "∀a∈set asx'. intra_kind (kind a)"
        by blast
      from ‹as = asx@a'#asx'› have "a#as = (a#asx)@a'#asx'" by simp
      moreover
      from ‹kind a = Q:r↪⇘p⇙fs› ‹same_level_path_aux (a#cs) asx›
      have "same_level_path_aux cs (a#asx)" by simp
      moreover
      from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs (a#cs) asx = c'#cs'›
      have "upd_cs cs (a#asx) = c'#cs'" by simp
      moreover
      from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs (a#cs) (asx@[a']) = []›
      have "upd_cs cs ((a#asx)@[a']) = []" by simp
      ultimately show ?case using assms by blast
    qed
  next
    case (slpa_Return cs a as Q p f c' cs')
    note IH = ‹⟦upd_cs cs' as = []; ∀c∈set cs'. valid_edge c; 
      ∀a'∈set as. valid_edge a'⟧ ⟹ 
      (∀a'∈set as. intra_kind (kind a')) ∨
      (∃asx a' asx' Q' p' f' c'' cs''. as = asx@a'#asx' ∧ 
        same_level_path_aux cs' asx ∧ kind a' = Q'↩⇘p'⇙f' ∧ upd_cs cs' asx = c''#cs'' ∧
        upd_cs cs' (asx@[a']) = [] ∧ a' ∈ get_return_edges c'' ∧ valid_edge c'' ∧ 
        (∀a'∈set asx'. intra_kind (kind a')))›
    from ‹∀a'∈set (a#as). valid_edge a'› have "valid_edge a" 
      and "∀a'∈set as. valid_edge a'" by simp_all
    from ‹∀c∈set cs. valid_edge c› ‹cs = c' # cs'›
    have "valid_edge c'" and "∀c∈set cs'. valid_edge c" by simp_all
    from ‹upd_cs cs (a#as) = []› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› 
      ‹a ∈ get_return_edges c'› have "upd_cs cs' as = []" by simp
    from IH[OF this ‹∀c∈set cs'. valid_edge c› ‹∀a'∈set as. valid_edge a'›] show ?case
    proof
      assume "∀a'∈set as. intra_kind (kind a')"
      hence "upd_cs cs' as = cs'" by(rule upd_cs_intra_path)
      with ‹upd_cs cs' as = []› have "cs' = []" by simp
      with ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› ‹kind a = Q↩⇘p⇙f›
      have "upd_cs cs [a] = []" by simp
      moreover
      from ‹cs = c'#cs'› have "upd_cs cs [] ≠ []" by simp
      moreover
      have "same_level_path_aux cs []" by simp
      ultimately show ?case 
        using ‹kind a = Q↩⇘p⇙f› ‹∀a'∈set as. intra_kind (kind a')› ‹cs = c'#cs'›
          ‹a ∈ get_return_edges c'› ‹valid_edge c'›
        by fastforce
    next
      assume "∃asx a' asx' Q' p' f' c'' cs''. as = asx@a'#asx' ∧
        same_level_path_aux cs' asx ∧ kind a' = Q'↩⇘p'⇙f' ∧ upd_cs cs' asx = c''#cs'' ∧
        upd_cs cs' (asx@[a']) = [] ∧ a' ∈ get_return_edges c'' ∧ valid_edge c'' ∧
        (∀a'∈set asx'. intra_kind (kind a'))"
      then obtain asx a' asx' Q' p' f' c'' cs'' where "as = asx@a'#asx'"
        and "same_level_path_aux cs' asx" and "upd_cs cs' asx = c''#cs''" 
        and "upd_cs cs' (asx@[a']) = []" and assms:"a' ∈ get_return_edges c''" 
        "kind a' = Q'↩⇘p'⇙f'" "valid_edge c''" "∀a'∈set asx'. intra_kind (kind a')"
        by blast
      from ‹as = asx@a'#asx'› have "a#as = (a#asx)@a'#asx'" by simp
      moreover
      from ‹same_level_path_aux cs' asx› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'›
        ‹kind a = Q↩⇘p⇙f›
      have "same_level_path_aux cs (a#asx)" by simp
      moreover
      from ‹upd_cs cs' asx = c''#cs''› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
      have "upd_cs cs (a#asx) = c''#cs''" by simp
      moreover
      from ‹upd_cs cs' (asx@[a']) = []› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'›
        ‹kind a = Q↩⇘p⇙f›
      have "upd_cs cs ((a#asx)@[a']) = []" by simp
      ultimately show ?case using assms by blast
    qed
  qed
qed


lemma same_level_path_aux_valid_path_aux: 
  "same_level_path_aux cs as ⟹ valid_path_aux cs as"
by(induct rule:slpa_induct,auto split:edge_kind.split simp:intra_kind_def)


lemma same_level_path_aux_Append:
  "⟦same_level_path_aux cs as; same_level_path_aux (upd_cs cs as) as'⟧
  ⟹ same_level_path_aux cs (as@as')"
by(induct rule:slpa_induct,auto simp:intra_kind_def)


lemma same_level_path_aux_callstack_Append:
  "same_level_path_aux cs as ⟹ same_level_path_aux (cs@cs') as"
by(induct rule:slpa_induct,auto simp:intra_kind_def)


lemma same_level_path_upd_cs_callstack_Append:
  "⟦same_level_path_aux cs as; upd_cs cs as = cs'⟧ 
  ⟹ upd_cs (cs@cs'') as = (cs'@cs'')"
by(induct rule:slpa_induct,auto split:edge_kind.split simp:intra_kind_def)


lemma slpa_split:
  assumes "same_level_path_aux cs as" and "as = xs@ys" and "upd_cs cs xs = []"
  shows "same_level_path_aux cs xs" and "same_level_path_aux [] ys"
using assms
proof(induct arbitrary:xs ys rule:slpa_induct)
  case (slpa_empty cs) case 1
  from ‹[] = xs@ys› show ?case by simp
next
  case (slpa_empty cs) case 2
  from ‹[] = xs@ys› show ?case by simp
next
  case (slpa_intra cs a as)
  note IH1 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs cs xs = []⟧ ⟹ same_level_path_aux cs xs›
  note IH2 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs cs xs = []⟧ ⟹ same_level_path_aux [] ys›
  { case 1
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = []› Cons ‹intra_kind (kind a)›
      have "upd_cs cs xs' = []" by(fastforce simp:intra_kind_def)
      from IH1[OF ‹as = xs'@ys› this] have "same_level_path_aux cs xs'" .
      with ‹a = x'› ‹intra_kind (kind a)› Cons
      show ?thesis by(fastforce simp:intra_kind_def)
    qed
  next
    case 2
    show ?case
    proof(cases xs)
      case Nil
      with ‹upd_cs cs xs = []› have "cs = []" by fastforce
      with Nil ‹a#as = xs@ys› ‹same_level_path_aux cs as› ‹intra_kind (kind a)›
      show ?thesis by(cases ys,auto simp:intra_kind_def)
    next
      case (Cons x' xs')
      with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = []› Cons ‹intra_kind (kind a)›
      have "upd_cs cs xs' = []" by(fastforce simp:intra_kind_def)
      from IH2[OF ‹as = xs'@ys› this] show ?thesis .
    qed
  }
next
  case (slpa_Call cs a as Q r p fs)
  note IH1 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs (a#cs) xs = []⟧ 
    ⟹ same_level_path_aux (a#cs) xs›
  note IH2 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs (a#cs) xs = []⟧ 
    ⟹ same_level_path_aux [] ys›
  { case 1
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = []› Cons ‹kind a = Q:r↪⇘p⇙fs›
      have "upd_cs (a#cs) xs' = []" by simp
      from IH1[OF ‹as = xs'@ys› this] have "same_level_path_aux (a#cs) xs'" .
      with ‹a = x'› ‹kind a = Q:r↪⇘p⇙fs› Cons show ?thesis by simp
    qed
  next
    case 2
    show ?case
    proof(cases xs)
      case Nil
      with ‹upd_cs cs xs = []› have "cs = []" by fastforce
      with Nil ‹a#as = xs@ys› ‹same_level_path_aux (a#cs) as› ‹kind a = Q:r↪⇘p⇙fs›
      show ?thesis by(cases ys) auto
    next
      case (Cons x' xs')
      with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = []› Cons ‹kind a = Q:r↪⇘p⇙fs›
      have "upd_cs (a#cs) xs' = []" by simp
      from IH2[OF ‹as = xs'@ys› this] show ?thesis .
    qed
  }
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH1 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs cs' xs = []⟧ ⟹ same_level_path_aux cs' xs›
  note IH2 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs cs' xs = []⟧ ⟹ same_level_path_aux [] ys›
  { case 1
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = []› Cons ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
      have "upd_cs cs' xs' = []" by simp
      from IH1[OF ‹as = xs'@ys› this] have "same_level_path_aux cs' xs'" .
      with ‹a = x'› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› Cons 
      show ?thesis by simp
    qed
  next
    case 2
    show ?case
    proof(cases xs)
      case Nil
      with ‹upd_cs cs xs = []› have "cs = []" by fastforce 
      with ‹cs = c'#cs'› have False by simp
      thus ?thesis by simp
    next
      case (Cons x' xs')
      with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = []› Cons ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
      have "upd_cs cs' xs' = []" by simp
      from IH2[OF ‹as = xs'@ys› this] show ?thesis .
    qed
  }
qed


lemma slpa_number_Calls_eq_number_Returns:
  "⟦same_level_path_aux cs as; upd_cs cs as = []; 
    ∀a ∈ set as. valid_edge a; ∀c ∈ set cs. valid_edge c⟧
  ⟹ length [a←as@cs. ∃Q r p fs. kind a = Q:r↪⇘p⇙fs] = 
     length [a←as. ∃Q p f. kind a = Q↩⇘p⇙f]"
apply(induct rule:slpa_induct)
by(auto split:list.split edge_kind.split intro:only_call_get_return_edges 
         simp:intra_kind_def)


lemma slpa_get_proc:
  "⟦same_level_path_aux cs as; upd_cs cs as = []; n -as→* n'; 
    ∀c ∈ set cs. valid_edge c⟧
  ⟹ (if cs = [] then get_proc n else get_proc(last(sourcenodes cs))) = get_proc n'"
proof(induct arbitrary:n rule:slpa_induct)
  case slpa_empty thus ?case by fastforce
next
  case (slpa_intra cs a as)
  note IH = ‹⋀n. ⟦upd_cs cs as = []; n -as→* n'; ∀a∈set cs. valid_edge a⟧
    ⟹ (if cs = [] then get_proc n else get_proc (last (sourcenodes cs))) = 
        get_proc n'›
  from ‹intra_kind (kind a)› ‹upd_cs cs (a#as) = []›
  have "upd_cs cs as = []" by(cases "kind a",auto simp:intra_kind_def)
  from ‹n -a#as→* n'› have "n -[]@a#as→* n'" by simp
  hence "valid_edge a" and "n = sourcenode a" and "targetnode a -as→* n'"
    by(fastforce dest:path_split)+
  from ‹valid_edge a› ‹intra_kind (kind a)› ‹ n = sourcenode a›
  have "get_proc n = get_proc (targetnode a)"
    by(fastforce intro:get_proc_intra)
  from IH[OF ‹upd_cs cs as = []› ‹targetnode a -as→* n'› ‹∀a∈set cs. valid_edge a›]
  have "(if cs = [] then get_proc (targetnode a) 
         else get_proc (last (sourcenodes cs))) = get_proc n'" .
  with ‹get_proc n = get_proc (targetnode a)› show ?case by auto
next
  case (slpa_Call cs a as Q r p fs)
  note IH = ‹⋀n. ⟦upd_cs (a#cs) as = []; n -as→* n'; ∀a∈set (a#cs). valid_edge a⟧
    ⟹ (if a#cs = [] then get_proc n else get_proc (last (sourcenodes (a#cs)))) = 
        get_proc n'›
  from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs cs (a#as) = []›
  have "upd_cs (a#cs) as = []" by simp
  from ‹n -a#as→* n'› have "n -[]@a#as→* n'" by simp
  hence "valid_edge a" and "n = sourcenode a" and "targetnode a -as→* n'"
    by(fastforce dest:path_split)+
  from ‹valid_edge a› ‹∀a∈set cs. valid_edge a› have "∀a∈set (a#cs). valid_edge a"
    by simp
  from IH[OF ‹upd_cs (a#cs) as = []› ‹targetnode a -as→* n'› this]
  have "get_proc (last (sourcenodes (a#cs))) = get_proc n'" by simp
  with ‹n = sourcenode a› show ?case by(cases cs,auto simp:sourcenodes_def)
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH = ‹⋀n. ⟦upd_cs cs' as = []; n -as→* n'; ∀a∈set cs'. valid_edge a⟧
    ⟹ (if cs' = [] then get_proc n else get_proc (last (sourcenodes cs'))) = 
       get_proc n'›
  from ‹∀a∈set cs. valid_edge a› ‹cs = c'#cs'›
  have "valid_edge c'" and "∀a∈set cs'. valid_edge a" by simp_all
  from ‹kind a = Q↩⇘p⇙f› ‹upd_cs cs (a#as) = []› ‹cs = c'#cs'›
  have "upd_cs cs' as = []" by simp
  from ‹n -a#as→* n'› have "n -[]@a#as→* n'" by simp
  hence "n = sourcenode a" and "targetnode a -as→* n'"
    by(fastforce dest:path_split)+
  from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
  have "get_proc (sourcenode c') = get_proc (targetnode a)"
    by(rule get_proc_get_return_edge)
  from IH[OF ‹upd_cs cs' as = []› ‹targetnode a -as→* n'› ‹∀a∈set cs'. valid_edge a›]
  have "(if cs' = [] then get_proc (targetnode a) 
         else get_proc (last (sourcenodes cs'))) = get_proc n'" .
  with ‹cs = c'#cs'› ‹get_proc (sourcenode c') = get_proc (targetnode a)›
  show ?case by(auto simp:sourcenodes_def)
qed


lemma slpa_get_return_edges:
  "⟦same_level_path_aux cs as; cs ≠ []; upd_cs cs as = [];
  ∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []⟧
  ⟹ last as ∈ get_return_edges (last cs)"
proof(induct rule:slpa_induct)
  case (slpa_empty cs)
  from ‹cs ≠ []› ‹upd_cs cs [] = []› have False by fastforce
  thus ?case by simp
next
  case (slpa_intra cs a as)
  note IH = ‹⟦cs ≠ []; upd_cs cs as = []; 
              ∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []⟧
    ⟹ last as ∈ get_return_edges (last cs)›
  show ?case
  proof(cases "as = []")
    case True
    with ‹intra_kind (kind a)› ‹upd_cs cs (a#as) = []› have "cs = []"
      by(fastforce simp:intra_kind_def)
    with ‹cs ≠ []› have False by simp
    thus ?thesis by simp
  next
    case False
    from ‹intra_kind (kind a)› ‹upd_cs cs (a#as) = []› have "upd_cs cs as = []"
      by(fastforce simp:intra_kind_def)
    from ‹∀xs ys. a#as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []› ‹intra_kind (kind a)›
    have "∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []"
      apply(clarsimp,erule_tac x="a#xs" in allE)
      by(auto simp:intra_kind_def)
    from IH[OF ‹cs ≠ []› ‹upd_cs cs as = []› this] 
    have "last as ∈ get_return_edges (last cs)" .
    with False show ?thesis by simp
  qed
next
  case (slpa_Call cs a as Q r p fs)
  note IH = ‹⟦a#cs ≠ []; upd_cs (a#cs) as = [];
    ∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs (a#cs) xs ≠ []⟧
    ⟹ last as ∈ get_return_edges (last (a#cs))›
  show ?case
  proof(cases "as = []")
    case True
    with ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs cs (a#as) = []› have "a#cs = []" by simp
    thus ?thesis by simp
  next
    case False
    from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs cs (a#as) = []› have "upd_cs (a#cs) as = []"
      by simp
    from ‹∀xs ys. a#as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []› ‹kind a = Q:r↪⇘p⇙fs›
    have "∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs (a#cs) xs ≠ []"
      by(clarsimp,erule_tac x="a#xs" in allE,simp)
    from IH[OF _ ‹upd_cs (a#cs) as = []› this] 
    have "last as ∈ get_return_edges (last (a#cs))" by simp
    with False ‹cs ≠ []› show ?thesis by(simp add:targetnodes_def)
  qed
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH = ‹⟦cs' ≠ []; upd_cs cs' as = []; 
    ∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs' xs ≠ []⟧
    ⟹ last as ∈ get_return_edges (last cs')›
  show ?case
  proof(cases "as = []")
    case True
    with ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹upd_cs cs (a#as) = []›
    have "cs' = []" by simp
    with ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› True
    show ?thesis by simp
  next
    case False
    from ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹upd_cs cs (a#as) = []›
    have "upd_cs cs' as = []" by simp
    show ?thesis
    proof(cases "cs' = []")
      case True
      with ‹cs = c'#cs'› ‹kind a = Q↩⇘p⇙f› have "upd_cs cs [a] = []" by simp
      with ‹∀xs ys. a#as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []› False have False
        apply(erule_tac x="[a]" in allE) by fastforce
      thus ?thesis by simp
    next
      case False
      from ‹∀xs ys. a#as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []›
        ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
      have "∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs' xs ≠ []"
        by(clarsimp,erule_tac x="a#xs" in allE,simp)
      from IH[OF False ‹upd_cs cs' as = []› this]
      have "last as ∈ get_return_edges (last cs')" .
      with ‹as ≠ []› False ‹cs = c'#cs'› show ?thesis by(simp add:targetnodes_def)
    qed
  qed
qed


lemma slpa_callstack_length:
  assumes "same_level_path_aux cs as" and "length cs = length cfsx"
  obtains cfx cfsx' where "transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs"
  and "transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs'"
  and "length cfsx' = length (upd_cs cs as)"
proof(atomize_elim)
  from assms show "∃cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs ∧
    transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' ∧
    length cfsx' = length (upd_cs cs as)"
  proof(induct arbitrary:cfsx cf rule:slpa_induct)
    case (slpa_empty cs) thus ?case by(simp add:kinds_def)
  next
    case (slpa_intra cs a as)
    note IH = ‹⋀cfsx cf. length cs = length cfsx ⟹
      ∃cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs ∧
                  transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' ∧
                  length cfsx' = length (upd_cs cs as)›
    from ‹intra_kind (kind a)› 
    have "length (upd_cs cs (a#as)) = length (upd_cs cs as)"
      by(fastforce simp:intra_kind_def)
    show ?case
    proof(cases cfsx)
      case Nil
      with ‹length cs = length cfsx› have "length cs = length []" by simp
      from Nil ‹intra_kind (kind a)› 
      obtain cfx where transfer:"transfer (kind a) (cfsx@cf#cfs) = []@cfx#cfs"
        "transfer (kind a) (cfsx@cf#cfs') = []@cfx#cfs'"
        by(cases "kind a",auto simp:kinds_def intra_kind_def)
      from IH[OF ‹length cs = length []›] obtain cfsx' cfx' 
        where "transfers (kinds as) ([]@cfx#cfs) = cfsx'@cfx'#cfs"
        and "transfers (kinds as) ([]@cfx#cfs') = cfsx'@cfx'#cfs'"
        and "length cfsx' = length (upd_cs cs as)" by blast
      with ‹length (upd_cs cs (a#as)) = length (upd_cs cs as)› transfer
      show ?thesis by(fastforce simp:kinds_def)
    next
      case (Cons x xs)
      with ‹intra_kind (kind a)› obtain cfx' 
        where transfer:"transfer (kind a) (cfsx@cf#cfs) = (cfx'#xs)@cf#cfs"
        "transfer (kind a) (cfsx@cf#cfs') = (cfx'#xs)@cf#cfs'"
        by(cases "kind a",auto simp:kinds_def intra_kind_def)
      from ‹length cs = length cfsx› Cons have "length cs = length (cfx'#xs)"
        by simp
      from IH[OF this] obtain cfs'' cf''
        where "transfers (kinds as) ((cfx'#xs)@cf#cfs) = cfs''@cf''#cfs"
        and "transfers (kinds as) ((cfx'#xs)@cf#cfs') = cfs''@cf''#cfs'"
        and "length cfs'' = length (upd_cs cs as)" by blast
      with ‹length (upd_cs cs (a#as)) = length (upd_cs cs as)› transfer
      show ?thesis by(fastforce simp:kinds_def)
    qed
  next
    case (slpa_Call cs a as Q r p fs)
    note IH = ‹⋀cfsx cf. length (a#cs) = length cfsx ⟹
      ∃cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs ∧
                  transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' ∧
                  length cfsx' = length (upd_cs (a#cs) as)›
    from ‹kind a = Q:r↪⇘p⇙fs›
    obtain cfx where transfer:"transfer (kind a) (cfsx@cf#cfs) = (cfx#cfsx)@cf#cfs"
      "transfer (kind a) (cfsx@cf#cfs') = (cfx#cfsx)@cf#cfs'"
      by(cases cfsx) auto
    from ‹length cs = length cfsx› have "length (a#cs) = length (cfx#cfsx)"
      by simp
    from IH[OF this] obtain cfsx' cfx' 
      where "transfers (kinds as) ((cfx#cfsx)@cf#cfs) = cfsx'@cfx'#cfs"
      and "transfers (kinds as) ((cfx#cfsx)@cf#cfs') = cfsx'@cfx'#cfs'"
      and "length cfsx' = length (upd_cs (a#cs) as)" by blast
    with ‹kind a = Q:r↪⇘p⇙fs› transfer show ?case by(fastforce simp:kinds_def)
  next
     case (slpa_Return cs a as Q p f c' cs')
     note IH = ‹⋀cfsx cf. length cs' = length cfsx ⟹
       ∃cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs ∧
                   transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' ∧
                   length cfsx' = length (upd_cs cs' as)›
     from ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
     have "length (upd_cs cs (a#as)) = length (upd_cs cs' as)" by simp
     show ?case
     proof(cases cs')
       case Nil
       with ‹cs = c'#cs'› ‹length cs = length cfsx› obtain cfx
         where [simp]:"cfsx = [cfx]" by(cases cfsx) auto
       with ‹kind a = Q↩⇘p⇙f› obtain cf' 
         where transfer:"transfer (kind a) (cfsx@cf#cfs) = []@cf'#cfs"
         "transfer (kind a) (cfsx@cf#cfs') = []@cf'#cfs'"
         by fastforce
       from Nil have "length cs' = length []" by simp
       from IH[OF this] obtain cfsx' cfx' 
         where "transfers (kinds as) ([]@cf'#cfs) = cfsx'@cfx'#cfs"
         and "transfers (kinds as) ([]@cf'#cfs') = cfsx'@cfx'#cfs'"
         and "length cfsx' = length (upd_cs cs' as)" by blast
       with ‹length (upd_cs cs (a#as)) = length (upd_cs cs' as)› transfer
       show ?thesis by(fastforce simp:kinds_def)
    next
      case (Cons cx csx)
      with ‹cs = c'#cs'› ‹length cs = length cfsx› obtain x x' xs
        where [simp]:"cfsx = x#x'#xs" and "length xs = length csx"
        by(cases cfsx,auto,case_tac list,fastforce+)
      with ‹kind a = Q↩⇘p⇙f› obtain cf' 
        where transfer:"transfer (kind a) ((x#x'#xs)@cf#cfs) = (cf'#xs)@cf#cfs"
        "transfer (kind a) ((x#x'#xs)@cf#cfs') = (cf'#xs)@cf#cfs'"
        by fastforce
      from ‹cs = c'#cs'› ‹length cs = length cfsx› have "length cs' = length (cf'#xs)"
        by simp
      from IH[OF this] obtain cfsx' cfx 
        where "transfers (kinds as) ((cf'#xs)@cf#cfs) = cfsx'@cfx#cfs"
        and "transfers (kinds as) ((cf'#xs)@cf#cfs') = cfsx'@cfx#cfs'"
        and "length cfsx' = length (upd_cs cs' as)" by blast
      with ‹length (upd_cs cs (a#as)) = length (upd_cs cs' as)› transfer
      show ?thesis by(fastforce simp:kinds_def)
    qed
  qed
qed


lemma slpa_snoc_intra:
  "⟦same_level_path_aux cs as; intra_kind (kind a)⟧ 
  ⟹ same_level_path_aux cs (as@[a])"
by(induct rule:slpa_induct,auto simp:intra_kind_def)


lemma slpa_snoc_Call:
  "⟦same_level_path_aux cs as; kind a = Q:r↪⇘p⇙fs⟧
  ⟹ same_level_path_aux cs (as@[a])"
by(induct rule:slpa_induct,auto simp:intra_kind_def)


lemma vpa_Main_slpa:
  "⟦valid_path_aux cs as; m -as→* m'; as ≠ []; 
    valid_call_list cs m; get_proc m' = Main;
    get_proc (case cs of [] ⇒ m | _ ⇒ sourcenode (last cs)) = Main⟧
  ⟹ same_level_path_aux cs as ∧ upd_cs cs as = []"
proof(induct arbitrary:m rule:vpa_induct)
  case (vpa_empty cs) thus ?case by simp
next
  case (vpa_intra cs a as)
  note IH = ‹⋀m. ⟦m -as→* m'; as ≠ []; valid_call_list cs m; get_proc m' = Main;
    get_proc (case cs of [] ⇒ m | a # list ⇒ sourcenode (last cs)) = Main⟧
    ⟹ same_level_path_aux cs as ∧ upd_cs cs as = []›
  from ‹m -a # as→* m'› have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
  from ‹valid_edge a› ‹intra_kind (kind a)› 
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  show ?case
  proof(cases "as = []")
    case True
    with ‹targetnode a -as→* m'› have "targetnode a = m'" by fastforce
    with ‹get_proc (sourcenode a) = get_proc (targetnode a)› 
      ‹sourcenode a = m› ‹get_proc m' = Main›
    have "get_proc m = Main" by simp
    have "cs = []"
    proof(cases cs)
      case Cons
      with ‹valid_call_list cs m›
      obtain c Q r p fs where "valid_edge c" and "kind c = Q:r↪⇘get_proc m⇙fs"
        by(auto simp:valid_call_list_def,erule_tac x="[]" in allE,
           auto simp:sourcenodes_def)
      with ‹get_proc m = Main› have "kind c = Q:r↪⇘Main⇙fs" by simp
      with ‹valid_edge c› have False by(rule Main_no_call_target)
      thus ?thesis by simp
    qed simp
    with True ‹intra_kind (kind a)› show ?thesis by(fastforce simp:intra_kind_def)
  next
    case False
    from ‹valid_call_list cs m› ‹sourcenode a = m›
      ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_call_list cs (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(erule_tac x="cs'" in allE)
      apply(erule_tac x="c" in allE)
      by(auto split:list.split)
    from ‹get_proc (case cs of [] ⇒ m | _ ⇒ sourcenode (last cs)) = Main›
      ‹sourcenode a = m› ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "get_proc (case cs of [] ⇒ targetnode a | _ ⇒ sourcenode (last cs)) = Main"
      by(cases cs) auto
    from IH[OF ‹targetnode a -as→* m'› False ‹valid_call_list cs (targetnode a)›
      ‹get_proc m' = Main› this]
    have "same_level_path_aux cs as ∧ upd_cs cs as = []" .
    with ‹intra_kind (kind a)› show ?thesis by(fastforce simp:intra_kind_def)
  qed
next
  case (vpa_Call cs a as Q r p fs)
  note IH = ‹⋀m. ⟦m -as→* m'; as ≠ []; valid_call_list (a # cs) m; 
    get_proc m' = Main; 
    get_proc (case a # cs of [] ⇒ m | _ ⇒ sourcenode (last (a # cs))) = Main⟧
    ⟹ same_level_path_aux (a # cs) as ∧ upd_cs (a # cs) as = []›
  from ‹m -a # as→* m'› have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
    by(rule get_proc_call)
  show ?case
  proof(cases "as = []")
    case True
    with ‹targetnode a -as→* m'› have "targetnode a = m'" by fastforce
    with ‹get_proc (targetnode a) = p› ‹get_proc m' = Main› ‹kind a = Q:r↪⇘p⇙fs›
    have "kind a = Q:r↪⇘Main⇙fs" by simp
    with ‹valid_edge a› have False by(rule Main_no_call_target)
    thus ?thesis by simp
  next
    case False
    from ‹get_proc (targetnode a) = p› ‹valid_call_list cs m› ‹valid_edge a›
      ‹kind a = Q:r↪⇘p⇙fs› ‹sourcenode a = m›
    have "valid_call_list (a # cs) (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:sourcenodes_def)
    from ‹get_proc (case cs of [] ⇒ m | _ ⇒ sourcenode (last cs)) = Main›
      ‹sourcenode a = m›
    have "get_proc (case a # cs of [] ⇒ targetnode a 
      | _ ⇒ sourcenode (last (a # cs))) = Main"
      by(cases cs) auto
    from IH[OF ‹targetnode a -as→* m'› False ‹valid_call_list (a#cs) (targetnode a)›
      ‹get_proc m' = Main› this]
    have "same_level_path_aux (a # cs) as ∧ upd_cs (a # cs) as = []" .
    with ‹kind a = Q:r↪⇘p⇙fs› show ?thesis by simp
  qed
next
  case (vpa_ReturnEmpty cs a as Q p f)
  note IH = ‹⋀m. ⟦m -as→* m'; as ≠ []; valid_call_list [] m; get_proc m' = Main;
    get_proc (case [] of [] ⇒ m | a # list ⇒ sourcenode (last [])) = Main⟧
    ⟹ same_level_path_aux [] as ∧ upd_cs [] as = []›
  from ‹m -a # as→* m'› have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p" 
    by(rule get_proc_return)
  from ‹get_proc (case cs of [] ⇒ m | a # list ⇒ sourcenode (last cs)) = Main›
    ‹cs = []›
  have "get_proc m = Main" by simp
  with ‹sourcenode a = m› ‹get_proc (sourcenode a) = p› have "p = Main" by simp
  with ‹kind a = Q↩⇘p⇙f› have "kind a = Q↩⇘Main⇙f" by simp
  with ‹valid_edge a› have False by(rule Main_no_return_source)
  thus ?case by simp
next
  case (vpa_ReturnCons cs a as Q p f c' cs')
  note IH = ‹⋀m. ⟦m -as→* m'; as ≠ []; valid_call_list cs' m; get_proc m' = Main;
    get_proc (case cs' of [] ⇒ m | a # list ⇒ sourcenode (last cs')) = Main⟧
    ⟹ same_level_path_aux cs' as ∧ upd_cs cs' as = []›
  from ‹m -a # as→* m'› have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p" 
    by(rule get_proc_return)
  from ‹valid_call_list cs m› ‹cs = c' # cs'›
  have "valid_edge c'" 
    by(auto simp:valid_call_list_def,erule_tac x="[]" in allE,auto)
  from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
  have "get_proc (sourcenode c') = get_proc (targetnode a)"
    by(rule get_proc_get_return_edge)
  show ?case
  proof(cases "as = []")
    case True
    with ‹targetnode a -as→* m'› have "targetnode a = m'" by fastforce
    with ‹get_proc m' = Main› have "get_proc (targetnode a) = Main" by simp
    from ‹get_proc (sourcenode c') = get_proc (targetnode a)›
      ‹get_proc (targetnode a) = Main›
    have "get_proc (sourcenode c') = Main" by simp
    have "cs' = []"
    proof(cases cs')
      case (Cons cx csx)
      with ‹cs = c' # cs'› ‹valid_call_list cs m›
      obtain Qx rx fsx where "valid_edge cx" 
        and "kind cx = Qx:rx↪⇘get_proc (sourcenode c')⇙fsx"
        by(auto simp:valid_call_list_def,erule_tac x="[c']" in allE,
           auto simp:sourcenodes_def)
      with ‹get_proc (sourcenode c') = Main› have "kind cx = Qx:rx↪⇘Main⇙fsx" by simp
      with ‹valid_edge cx› have False by(rule Main_no_call_target)
      thus ?thesis by simp
    qed simp
    with True ‹cs = c' # cs'› ‹a ∈ get_return_edges c'› ‹kind a = Q↩⇘p⇙f›
    show ?thesis by simp
  next
    case False
    from ‹valid_call_list cs m› ‹cs = c' # cs'›
      ‹get_proc (sourcenode c') = get_proc (targetnode a)›
    have "valid_call_list cs' (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(hypsubst_thin)
      apply(erule_tac x="c' # cs'" in allE)
      by(case_tac cs')(auto simp:sourcenodes_def)
    from ‹get_proc (case cs of [] ⇒ m | a # list ⇒ sourcenode (last cs)) = Main›
      ‹cs = c' # cs'› ‹get_proc (sourcenode c') = get_proc (targetnode a)›
    have "get_proc (case cs' of [] ⇒ targetnode a 
      | _ ⇒ sourcenode (last cs')) = Main"
      by(cases cs') auto
    from IH[OF ‹targetnode a -as→* m'› False ‹valid_call_list cs' (targetnode a)›
      ‹get_proc m' = Main› this]
    have "same_level_path_aux cs' as ∧ upd_cs cs' as = []" .
    with ‹kind a = Q↩⇘p⇙f› ‹cs = c' # cs'› ‹a ∈ get_return_edges c'›
    show ?thesis by simp
  qed
qed



definition same_level_path :: "'edge list ⇒ bool"
  where "same_level_path as ≡ same_level_path_aux [] as ∧ upd_cs [] as = []"


lemma same_level_path_valid_path:
  "same_level_path as ⟹ valid_path as"
by(fastforce intro:same_level_path_aux_valid_path_aux
             simp:same_level_path_def valid_path_def)


lemma same_level_path_Append:
  "⟦same_level_path as; same_level_path as'⟧ ⟹ same_level_path (as@as')"
by(fastforce elim:same_level_path_aux_Append upd_cs_Append simp:same_level_path_def)


lemma same_level_path_number_Calls_eq_number_Returns:
  "⟦same_level_path as; ∀a ∈ set as. valid_edge a⟧ ⟹ 
  length [a←as. ∃Q r p fs. kind a = Q:r↪⇘p⇙fs] = length [a←as. ∃Q p f. kind a = Q↩⇘p⇙f]"
by(fastforce dest:slpa_number_Calls_eq_number_Returns simp:same_level_path_def)


lemma same_level_path_valid_path_Append:
  "⟦same_level_path as; valid_path as'⟧ ⟹ valid_path (as@as')"
  by(fastforce intro:valid_path_aux_Append elim:same_level_path_aux_valid_path_aux
               simp:valid_path_def same_level_path_def)

lemma valid_path_same_level_path_Append:
  "⟦valid_path as; same_level_path as'⟧ ⟹ valid_path (as@as')"
  apply(auto simp:valid_path_def same_level_path_def)
  apply(erule valid_path_aux_Append)
  by(fastforce intro!:same_level_path_aux_valid_path_aux 
                dest:same_level_path_aux_callstack_Append)

lemma intras_same_level_path:
  assumes "∀a ∈ set as. intra_kind(kind a)" shows "same_level_path as"
proof -
  from ‹∀a ∈ set as. intra_kind(kind a)› have "same_level_path_aux [] as"
    by(induct as)(auto simp:intra_kind_def)
  moreover
  from ‹∀a ∈ set as. intra_kind(kind a)› have "upd_cs [] as = []"
    by(induct as)(auto simp:intra_kind_def)
  ultimately show ?thesis by(simp add:same_level_path_def)
qed


definition same_level_path' :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool" 
  ("_ -_→⇘sl⇙* _" [51,0,0] 80)
where slp_def:"n -as→⇘sl⇙* n' ≡ n -as→* n' ∧ same_level_path as"

lemma slp_vp: "n -as→⇘sl⇙* n' ⟹ n -as→⇩√* n'"
by(fastforce intro:same_level_path_valid_path simp:slp_def vp_def)


lemma intra_path_slp: "n -as→⇩ι* n' ⟹ n -as→⇘sl⇙* n'"
by(fastforce intro:intras_same_level_path simp:slp_def intra_path_def)


lemma slp_Append:
  "⟦n -as→⇘sl⇙* n''; n'' -as'→⇘sl⇙* n'⟧ ⟹ n -as@as'→⇘sl⇙* n'"
  by(fastforce simp:slp_def intro:path_Append same_level_path_Append)


lemma slp_vp_Append:
  "⟦n -as→⇘sl⇙* n''; n'' -as'→⇩√* n'⟧ ⟹ n -as@as'→⇩√* n'"
  by(fastforce simp:slp_def vp_def intro:path_Append same_level_path_valid_path_Append)


lemma vp_slp_Append:
  "⟦n -as→⇩√* n''; n'' -as'→⇘sl⇙* n'⟧ ⟹ n -as@as'→⇩√* n'"
  by(fastforce simp:slp_def vp_def intro:path_Append valid_path_same_level_path_Append)


lemma slp_get_proc:
  "n -as→⇘sl⇙* n' ⟹ get_proc n = get_proc n'"
by(fastforce dest:slpa_get_proc simp:same_level_path_def slp_def)


lemma same_level_path_inner_path:
  assumes "n -as→⇘sl⇙* n'"
  obtains as' where "n -as'→⇩ι* n'" and "set(sourcenodes as') ⊆ set(sourcenodes as)"
proof(atomize_elim)
  from ‹n -as→⇘sl⇙* n'› have "n -as→* n'" and "same_level_path as"
    by(simp_all add:slp_def)
  from ‹same_level_path as› have "same_level_path_aux [] as" and "upd_cs [] as = []"
    by(simp_all add:same_level_path_def)
  from ‹n -as→* n'› ‹same_level_path_aux [] as› ‹upd_cs [] as = []›
  show "∃as'. n -as'→⇩ι* n' ∧ set(sourcenodes as') ⊆ set(sourcenodes as)"
  proof(induct as arbitrary:n rule:length_induct)
    fix as n
    assume IH:"∀as''. length as'' < length as ⟶
      (∀n''. n'' -as''→* n' ⟶ same_level_path_aux [] as'' ⟶
           upd_cs [] as'' = [] ⟶
           (∃as'. n'' -as'→⇩ι* n' ∧ set (sourcenodes as') ⊆ set (sourcenodes as'')))"
      and "n -as→* n'" and "same_level_path_aux [] as" and "upd_cs [] as = []"
    show "∃as'. n -as'→⇩ι* n' ∧ set (sourcenodes as') ⊆ set (sourcenodes as)"
    proof(cases as)
      case Nil
      with ‹n -as→* n'› show ?thesis by(fastforce simp:intra_path_def)
    next
      case (Cons a' as')
      with ‹n -as→* n'› Cons have "n = sourcenode a'" and "valid_edge a'" 
        and "targetnode a' -as'→* n'"
        by(auto intro:path_split_Cons)
      show ?thesis
      proof(cases "kind a'" rule:edge_kind_cases)
        case Intra
        with Cons ‹same_level_path_aux [] as› have "same_level_path_aux [] as'"
          by(fastforce simp:intra_kind_def)
        moreover
        from Intra Cons ‹upd_cs [] as = []› have "upd_cs [] as' = []"
          by(fastforce simp:intra_kind_def)
        ultimately obtain as'' where "targetnode a' -as''→⇩ι* n'"
          and "set (sourcenodes as'') ⊆ set (sourcenodes as')"
          using IH Cons ‹targetnode a' -as'→* n'›
          by(erule_tac x="as'" in allE) auto
        from ‹n = sourcenode a'› ‹valid_edge a'› Intra ‹targetnode a' -as''→⇩ι* n'›
        have "n -a'#as''→⇩ι* n'" by(fastforce intro:Cons_path simp:intra_path_def)
        with ‹set (sourcenodes as'') ⊆ set (sourcenodes as')› Cons show ?thesis
          by(rule_tac x="a'#as''" in exI,auto simp:sourcenodes_def)
      next
        case (Call Q p f)
        with Cons ‹same_level_path_aux [] as›
        have "same_level_path_aux [a'] as'" by simp
        from Call Cons ‹upd_cs [] as = []› have "upd_cs [a'] as' = []" by simp
        hence "as' ≠ []" by fastforce
        with ‹upd_cs [a'] as' = []› obtain xs ys where "as' = xs@ys" and "xs ≠ []"
        and "upd_cs [a'] xs = []" and "upd_cs [] ys = []"
        and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs [a'] xs' ≠ []"
          by -(erule upd_cs_empty_split,auto)
        from ‹same_level_path_aux [a'] as'› ‹as' = xs@ys› ‹upd_cs [a'] xs = []›
        have "same_level_path_aux [a'] xs" and "same_level_path_aux [] ys"
          by(auto intro:slpa_split)
        from ‹same_level_path_aux [a'] xs› ‹upd_cs [a'] xs = []›
          ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs [a'] xs' ≠ []›
        have "last xs ∈ get_return_edges (last [a'])"
          by(fastforce intro!:slpa_get_return_edges)
        with ‹valid_edge a'› Call
        obtain a where "valid_edge a" and "sourcenode a = sourcenode a'"
          and "targetnode a = targetnode (last xs)" and "kind a = (λcf. False)⇩√"
          by -(drule call_return_node_edge,auto)
        from ‹targetnode a = targetnode (last xs)› ‹xs ≠ []›
        have "targetnode a = targetnode (last (a'#xs))" by simp
        from ‹as' = xs@ys› ‹xs ≠ []› Cons have "length ys < length as" by simp
        from ‹targetnode a' -as'→* n'› ‹as' = xs@ys› ‹xs ≠ []›
        have "targetnode (last (a'#xs)) -ys→* n'"
          by(cases xs rule:rev_cases,auto dest:path_split)
        with IH ‹length ys < length as› ‹same_level_path_aux [] ys›
          ‹upd_cs [] ys = []›
        obtain as'' where "targetnode (last (a'#xs)) -as''→⇩ι* n'"
          and "set(sourcenodes as'') ⊆ set(sourcenodes ys)"
          apply(erule_tac x="ys" in allE) apply clarsimp
          apply(erule_tac x="targetnode (last (a'#xs))" in allE) 
          by clarsimp
        from ‹sourcenode a = sourcenode a'› ‹n = sourcenode a'›
          ‹targetnode a = targetnode (last (a'#xs))› ‹valid_edge a›
          ‹kind a = (λcf. False)⇩√› ‹targetnode (last (a'#xs)) -as''→⇩ι* n'›
        have "n -a#as''→⇩ι* n'"
          by(fastforce intro:Cons_path simp:intra_path_def intra_kind_def)
        moreover
        from ‹set(sourcenodes as'') ⊆ set(sourcenodes ys)› Cons ‹as' = xs@ys›
          ‹sourcenode a = sourcenode a'›
        have "set(sourcenodes (a#as'')) ⊆ set(sourcenodes as)"
          by(auto simp:sourcenodes_def)
        ultimately show ?thesis by blast
      next
        case (Return Q p f)
        with Cons ‹same_level_path_aux [] as› have False by simp
        thus ?thesis by simp
      qed
    qed
  qed
qed


lemma slp_callstack_length_equal:
  assumes "n -as→⇘sl⇙* n'" obtains cf' where "transfers (kinds as) (cf#cfs) = cf'#cfs"
  and "transfers (kinds as) (cf#cfs') = cf'#cfs'"
proof(atomize_elim)
  from ‹n -as→⇘sl⇙* n'› have "same_level_path_aux [] as" and "upd_cs [] as = []"
    by(simp_all add:slp_def same_level_path_def)
  then obtain cfx cfsx where "transfers (kinds as) (cf#cfs) = cfsx@cfx#cfs"
    and "transfers (kinds as) (cf#cfs') = cfsx@cfx#cfs'"
    and "length cfsx = length (upd_cs [] as)"
    by(fastforce elim:slpa_callstack_length)
  with ‹upd_cs [] as = []› have "cfsx = []" by(cases cfsx) auto
  with ‹transfers (kinds as) (cf#cfs) = cfsx@cfx#cfs›
    ‹transfers (kinds as) (cf#cfs') = cfsx@cfx#cfs'›
  show "∃cf'. transfers (kinds as) (cf#cfs) = cf'#cfs ∧ 
    transfers (kinds as) (cf#cfs') = cf'#cfs'" by fastforce
qed


lemma slp_cases [consumes 1,case_names intra_path return_intra_path]:
  assumes "m -as→⇘sl⇙* m'"
  obtains "m -as→⇩ι* m'"
  | as' a as'' Q p f where "as = as'@a#as''" and "kind a = Q↩⇘p⇙f"
  and "m -as'@[a]→⇘sl⇙* targetnode a" and "targetnode a -as''→⇩ι* m'"
proof(atomize_elim)
  from ‹m -as→⇘sl⇙* m'› have "m -as→* m'" and "same_level_path_aux [] as"
    and "upd_cs [] as = []" by(simp_all add:slp_def same_level_path_def)
  from ‹m -as→* m'› have "∀a ∈ set as. valid_edge a" by(rule path_valid_edges)
  have "∀a ∈ set []. valid_edge a" by simp
  with ‹same_level_path_aux [] as› ‹upd_cs [] as = []› ‹∀a ∈ set []. valid_edge a›
    ‹∀a ∈ set as. valid_edge a›
  show "m -as→⇩ι* m' ∨
    (∃as' a as'' Q p f. as = as' @ a # as'' ∧ kind a = Q↩⇘p⇙f ∧
    m -as' @ [a]→⇘sl⇙* targetnode a ∧ targetnode a -as''→⇩ι* m')"
  proof(cases rule:slpa_cases)
    case intra_path
    with ‹m -as→* m'› have "m -as→⇩ι* m'" by(simp add:intra_path_def)
    thus ?thesis by blast
  next
    case (return_intra_path as' a as'' Q p f c' cs')
    from ‹m -as→* m'› ‹as = as' @ a # as''›
    have "m -as'→* sourcenode a" and "valid_edge a" and "targetnode a -as''→* m'"
      by(auto intro:path_split)
    from ‹m -as'→* sourcenode a› ‹valid_edge a›
    have "m -as'@[a]→* targetnode a" by(fastforce intro:path_Append path_edge)
    with ‹same_level_path_aux [] as'› ‹upd_cs [] as' = c' # cs'› ‹kind a = Q↩⇘p⇙f›
      ‹a ∈ get_return_edges c'›
    have "same_level_path_aux [] (as'@[a])"
      by(fastforce intro:same_level_path_aux_Append)
    with ‹upd_cs [] (as' @ [a]) = []› ‹m -as'@[a]→* targetnode a›
    have "m -as'@[a]→⇘sl⇙* targetnode a" by(simp add:slp_def same_level_path_def)
    moreover
    from ‹∀a∈set as''. intra_kind (kind a)› ‹targetnode a -as''→* m'›
    have "targetnode a -as''→⇩ι* m'" by(simp add:intra_path_def)
    ultimately show ?thesis using ‹as = as' @ a # as''› ‹kind a = Q↩⇘p⇙f› by blast
  qed
qed


function same_level_path_rev_aux :: "'edge list ⇒ 'edge list ⇒ bool"
  where "same_level_path_rev_aux cs [] ⟷ True"
  | "same_level_path_rev_aux cs (as@[a]) ⟷ 
       (case (kind a) of Q↩⇘p⇙f ⇒ same_level_path_rev_aux (a#cs) as
                       | Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ False
                                     | c'#cs' ⇒ c' ∈ get_return_edges a ∧
                                             same_level_path_rev_aux cs' as
                       |    _ ⇒ same_level_path_rev_aux cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order


lemma slpra_induct [consumes 1,case_names slpra_empty slpra_intra slpra_Return
  slpra_Call]:
  assumes major: "same_level_path_rev_aux xs ys"
  and rules: "⋀cs. P cs []"
    "⋀cs a as. ⟦intra_kind(kind a); same_level_path_rev_aux cs as; P cs as⟧ 
      ⟹ P cs (as@[a])"
    "⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; same_level_path_rev_aux (a#cs) as; P (a#cs) as⟧ 
      ⟹ P cs (as@[a])"
    "⋀cs a as Q r p fs c' cs'. ⟦kind a = Q:r↪⇘p⇙fs; cs = c'#cs'; 
                   same_level_path_rev_aux cs' as; c' ∈ get_return_edges a; P cs' as⟧
     ⟹ P cs (as@[a])"
  shows "P xs ys"
using major
apply(induct ys arbitrary: xs rule:rev_induct)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)


lemma same_level_path_rev_aux_Append:
  "⟦same_level_path_rev_aux cs as'; same_level_path_rev_aux (upd_rev_cs cs as') as⟧
  ⟹ same_level_path_rev_aux cs (as@as')"
by(induct rule:slpra_induct,
   auto simp:intra_kind_def simp del:append_assoc simp:append_assoc[THEN sym])


lemma slpra_to_slpa:
  "⟦same_level_path_rev_aux cs as; upd_rev_cs cs as = []; n -as→* n'; 
  valid_return_list cs n'⟧
  ⟹ same_level_path_aux [] as ∧ same_level_path_aux (upd_cs [] as) cs ∧
     upd_cs (upd_cs [] as) cs = []"
proof(induct arbitrary:n' rule:slpra_induct)
  case slpra_empty thus ?case by simp
next
  case (slpra_intra cs a as)
  note IH = ‹⋀n'. ⟦upd_rev_cs cs as = []; n -as→* n'; valid_return_list cs n'⟧
    ⟹ same_level_path_aux [] as ∧ same_level_path_aux (upd_cs [] as) cs ∧
       upd_cs (upd_cs [] as) cs = []›
  from ‹n -as@[a]→* n'› have "n -as→* sourcenode a" and "valid_edge a"
    and "n' = targetnode a" by(auto intro:path_split_snoc)
  from ‹valid_edge a› ‹intra_kind (kind a)›
  have "get_proc (sourcenode a) = get_proc (targetnode a)"
    by(rule get_proc_intra)
  with ‹valid_return_list cs n'› ‹n' = targetnode a›
  have "valid_return_list cs (sourcenode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="cs'" in allE) apply clarsimp
    by(case_tac cs')(auto simp:targetnodes_def)
  from ‹upd_rev_cs cs (as@[a]) = []› ‹intra_kind (kind a)›
  have "upd_rev_cs cs as = []" by(fastforce simp:intra_kind_def)
  from ‹valid_edge a› ‹intra_kind (kind a)›
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  from IH[OF ‹upd_rev_cs cs as = []› ‹n -as→* sourcenode a›
    ‹valid_return_list cs (sourcenode a)›]
  have "same_level_path_aux [] as" 
    and "same_level_path_aux (upd_cs [] as) cs"
    and "upd_cs (upd_cs [] as) cs = []" by simp_all
  from ‹same_level_path_aux [] as› ‹intra_kind (kind a)›
  have "same_level_path_aux [] (as@[a])" by(rule slpa_snoc_intra)
  from ‹intra_kind (kind a)›
  have "upd_cs [] (as@[a]) = upd_cs [] as"
    by(fastforce simp:upd_cs_Append intra_kind_def)
  moreover
  from ‹same_level_path_aux [] as› ‹intra_kind (kind a)›
  have "same_level_path_aux [] (as@[a])" by(rule slpa_snoc_intra)
  ultimately show ?case using ‹same_level_path_aux (upd_cs [] as) cs›
    ‹upd_cs (upd_cs [] as) cs = []›
    by simp
next
  case (slpra_Return cs a as Q p f)
  note IH = ‹⋀n' n''. ⟦upd_rev_cs (a#cs) as = []; n -as→* n';
    valid_return_list (a#cs) n'⟧
  ⟹ same_level_path_aux [] as ∧
     same_level_path_aux (upd_cs [] as) (a#cs) ∧
     upd_cs (upd_cs [] as) (a#cs) = []›
  from ‹n -as@[a]→* n'› have "n -as→* sourcenode a" and "valid_edge a"
    and "n' = targetnode a" by(auto intro:path_split_snoc)
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "p = get_proc (sourcenode a)"
     by(rule get_proc_return[THEN sym])
   from ‹valid_return_list cs n'› ‹n' = targetnode a›
   have "valid_return_list cs (targetnode a)" by simp
   with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹p = get_proc (sourcenode a)›
   have "valid_return_list (a#cs) (sourcenode a)"
     apply(clarsimp simp:valid_return_list_def)
     apply(case_tac cs') apply auto
     apply(erule_tac x="list" in allE) apply clarsimp
     by(case_tac list,auto simp:targetnodes_def)
   from ‹upd_rev_cs cs (as@[a]) = []› ‹kind a = Q↩⇘p⇙f›
   have "upd_rev_cs (a#cs) as = []" by simp
   from IH[OF this ‹n -as→* sourcenode a› ‹valid_return_list (a#cs) (sourcenode a)›]
   have "same_level_path_aux [] as"
     and "same_level_path_aux (upd_cs [] as) (a#cs)"
     and "upd_cs (upd_cs [] as) (a#cs) = []" by simp_all
   show ?case 
  proof(cases "upd_cs [] as")
    case Nil
    with ‹kind a = Q↩⇘p⇙f› ‹same_level_path_aux (upd_cs [] as) (a#cs)›
    have False by simp
    thus ?thesis by simp
  next
    case (Cons cx csx)
    with ‹kind a = Q↩⇘p⇙f› ‹same_level_path_aux (upd_cs [] as) (a#cs)›
    obtain Qx fx 
      where match:"a ∈ get_return_edges cx" "same_level_path_aux csx cs" by auto
    from ‹kind a = Q↩⇘p⇙f› Cons have "upd_cs [] (as@[a]) = csx"
      by(rule upd_cs_snoc_Return_Cons)
    with ‹same_level_path_aux (upd_cs [] as) (a#cs)›
      ‹kind a = Q↩⇘p⇙f› match
    have "same_level_path_aux (upd_cs [] (as@[a])) cs" by simp
    from ‹upd_cs [] (as@[a]) = csx› ‹kind a = Q↩⇘p⇙f› Cons
      ‹upd_cs (upd_cs [] as) (a#cs) = []›
    have "upd_cs (upd_cs [] (as@[a])) cs = []" by simp
    from Cons ‹kind a = Q↩⇘p⇙f› match
    have "same_level_path_aux (upd_cs [] as) [a]" by simp
    with ‹same_level_path_aux [] as› have "same_level_path_aux [] (as@[a])"
      by(rule same_level_path_aux_Append)
    with ‹same_level_path_aux (upd_cs [] (as@[a])) cs›
      ‹upd_cs (upd_cs [] (as@[a])) cs = []›
    show ?thesis by simp
  qed
next
  case (slpra_Call cs a as Q r p fs cx csx)
  note IH = ‹⋀n'. ⟦upd_rev_cs csx as = []; n -as→* n'; valid_return_list csx n'⟧
    ⟹ same_level_path_aux [] as ∧
       same_level_path_aux (upd_cs [] as) csx ∧ upd_cs (upd_cs [] as) csx = []›
  note match = ‹cs = cx#csx› ‹cx ∈ get_return_edges a›
  from ‹n -as@[a]→* n'› have "n -as→* sourcenode a" and "valid_edge a"
    and "n' = targetnode a" by(auto intro:path_split_snoc)
  from ‹valid_edge a› match 
  have "get_proc (sourcenode a) = get_proc (targetnode cx)"
    by(fastforce intro:get_proc_get_return_edge)
  with ‹valid_return_list cs n'› ‹cs = cx#csx›
  have "valid_return_list csx (sourcenode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="cx#cs'" in allE) apply clarsimp
    by(case_tac cs',auto simp:targetnodes_def)
  from ‹kind a = Q:r↪⇘p⇙fs› match ‹upd_rev_cs cs (as@[a]) = []›
  have "upd_rev_cs csx as = []" by simp
  from IH[OF this ‹n -as→* sourcenode a› ‹valid_return_list csx (sourcenode a)›]
  have "same_level_path_aux [] as"
    and "same_level_path_aux (upd_cs [] as) csx" and "upd_cs (upd_cs [] as) csx = []"
    by simp_all
  from ‹same_level_path_aux [] as› ‹kind a = Q:r↪⇘p⇙fs›
  have "same_level_path_aux [] (as@[a])" by(rule slpa_snoc_Call)
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› match obtain Q' f' where "kind cx = Q'↩⇘p⇙f'"
    by(fastforce dest!:call_return_edges)
  from ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs [] (as@[a]) = a#(upd_cs [] as)"
    by(rule upd_cs_snoc_Call)
  with ‹same_level_path_aux (upd_cs [] as) csx› ‹kind a = Q:r↪⇘p⇙fs› 
    ‹kind cx = Q'↩⇘p⇙f'› match
  have "same_level_path_aux (upd_cs [] (as@[a])) cs" by simp
  from ‹upd_cs (upd_cs [] as) csx = []› ‹upd_cs [] (as@[a]) = a#(upd_cs [] as)›
    ‹kind a = Q:r↪⇘p⇙fs› ‹kind cx = Q'↩⇘p⇙f'› match
  have "upd_cs (upd_cs [] (as@[a])) cs = []" by simp
  with ‹same_level_path_aux [] (as@[a])›
    ‹same_level_path_aux (upd_cs [] (as@[a])) cs› show ?case by simp
qed


subsubsection ‹Lemmas on paths with ‹(_Entry_)››

lemma path_Entry_target [dest]:
  assumes "n -as→* (_Entry_)"
  shows "n = (_Entry_)" and "as = []"
using ‹n -as→* (_Entry_)›
proof(induct n as n'≡"(_Entry_)" rule:path.induct)
  case (Cons_path n'' as a n)
  from ‹n'' = (_Entry_)› ‹targetnode a = n''› ‹valid_edge a› have False
    by -(rule Entry_target,simp_all)
  { case 1
    from ‹False› show ?case ..
  next
    case 2
    from ‹False› show ?case ..
  }
qed simp_all



lemma Entry_sourcenode_hd:
  assumes "n -as→* n'" and "(_Entry_) ∈ set (sourcenodes as)"
  shows "n = (_Entry_)" and "(_Entry_) ∉ set (sourcenodes (tl as))"
  using ‹n -as→* n'› ‹(_Entry_) ∈ set (sourcenodes as)›
proof(induct rule:path.induct)
  case (empty_path n) case 1
  thus ?case by(simp add:sourcenodes_def)
next
  case (empty_path n) case 2
  thus ?case by(simp add:sourcenodes_def)
next
  case (Cons_path n'' as n' a n)
  note IH1 = ‹(_Entry_) ∈ set(sourcenodes as) ⟹ n'' = (_Entry_)›
  note IH2 = ‹(_Entry_) ∈ set(sourcenodes as) ⟹ (_Entry_) ∉ set(sourcenodes(tl as))›
  have "(_Entry_) ∉ set (sourcenodes(tl(a#as)))"
  proof(rule ccontr)
    assume "¬ (_Entry_) ∉ set (sourcenodes (tl (a#as)))"
    hence "(_Entry_) ∈ set (sourcenodes as)" by simp
    from IH1[OF this] have "n'' = (_Entry_)" by simp
    with ‹targetnode a = n''› ‹valid_edge a› show False by -(erule Entry_target,simp)
  qed
  hence "(_Entry_) ∉ set (sourcenodes(tl(a#as)))" by fastforce
  { case 1
    with ‹(_Entry_) ∉ set (sourcenodes(tl(a#as)))› ‹sourcenode a = n›
    show ?case by(simp add:sourcenodes_def)
  next
    case 2
    with ‹(_Entry_) ∉ set (sourcenodes(tl(a#as)))› ‹sourcenode a = n›
    show ?case by(simp add:sourcenodes_def)
  }
qed


lemma Entry_no_inner_return_path: 
  assumes "(_Entry_) -as@[a]→* n" and "∀a ∈ set as. intra_kind(kind a)"
  and "kind a = Q↩⇘p⇙f"
  shows "False"
proof -
  from ‹(_Entry_) -as@[a]→* n› have "(_Entry_) -as→* sourcenode a" 
    and "valid_edge a" and "targetnode a = n" by(auto intro:path_split_snoc)
  from ‹(_Entry_) -as→* sourcenode a› ‹∀a ∈ set as. intra_kind(kind a)›
  have "(_Entry_) -as→⇩ι* sourcenode a" by(simp add:intra_path_def)
  hence "get_proc (sourcenode a) = Main"
    by(fastforce dest:intra_path_get_procs simp:get_proc_Entry)
  with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "p = Main"
    by(fastforce dest:get_proc_return)
  with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› show ?thesis
    by(fastforce intro:Main_no_return_source)
qed



lemma vpra_no_slpra:
  "⟦valid_path_rev_aux cs as; n -as→* n'; valid_return_list cs n'; cs ≠ [];
    ∀xs ys. as = xs@ys ⟶ (¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ [])⟧
  ⟹ ∃a Q f. valid_edge a ∧ kind a = Q↩⇘get_proc n⇙f"
proof(induct arbitrary:n' rule:vpra_induct)
  case (vpra_empty cs)
  from ‹valid_return_list cs n'› ‹cs ≠ []› obtain Q f where "valid_edge (hd cs)"
    and "kind (hd cs) = Q↩⇘get_proc n'⇙f"
    apply(unfold valid_return_list_def)
    apply(drule hd_Cons_tl[THEN sym])
    apply(erule_tac x="[]" in allE) 
    apply(erule_tac x="hd cs" in allE)
    by auto
  from ‹n -[]→* n'› have "n = n'" by fastforce
  with ‹valid_edge (hd cs)› ‹kind (hd cs) = Q↩⇘get_proc n'⇙f› show ?case by blast
next
  case (vpra_intra cs a as)
  note IH = ‹⋀n'. ⟦n -as→* n'; valid_return_list cs n'; cs ≠ [];
    ∀xs ys. as = xs@ys ⟶ ¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []⟧
    ⟹ ∃a Q f. valid_edge a ∧ kind a = Q↩⇘get_proc n⇙f›
  note all = ‹∀xs ys. as@[a] = xs@ys 
    ⟶ ¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []›
  from ‹n -as@[a]→* n'› have "n -as→* sourcenode a" and "valid_edge a"
    and "targetnode a = n'" by(auto intro:path_split_snoc)
  from ‹valid_return_list cs n'› ‹cs ≠ []› obtain Q f where "valid_edge (hd cs)"
    and "kind (hd cs) = Q↩⇘get_proc n'⇙f"
    apply(unfold valid_return_list_def)
    apply(drule hd_Cons_tl[THEN sym])
    apply(erule_tac x="[]" in allE) 
    apply(erule_tac x="hd cs" in allE)
    by auto
  from ‹valid_edge a› ‹intra_kind (kind a)›
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  with ‹kind (hd cs) = Q↩⇘get_proc n'⇙f› ‹targetnode a = n'›
  have "kind (hd cs) = Q↩⇘get_proc (sourcenode a)⇙f" by simp
  from ‹valid_return_list cs n'› ‹targetnode a = n'›
    ‹get_proc (sourcenode a) = get_proc (targetnode a)›
  have "valid_return_list cs (sourcenode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="cs'" in allE)
    apply(erule_tac x="c" in allE)
    by(auto split:list.split)
  from all ‹intra_kind (kind a)›
  have "∀xs ys. as = xs@ys 
    ⟶ ¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []"
    apply clarsimp apply(erule_tac x="xs" in allE)
    by(auto simp:intra_kind_def)
  from IH[OF ‹n -as→* sourcenode a› ‹valid_return_list cs (sourcenode a)›
    ‹cs ≠ []› this] show ?case .
next
  case (vpra_Return cs a as Q p f)
  note IH = ‹⋀n'. ⟦n -as→* n'; valid_return_list (a#cs) n'; a#cs ≠ [];
   ∀xs ys. as = xs @ ys ⟶
    ¬ same_level_path_rev_aux (a#cs) ys ∨ upd_rev_cs (a#cs) ys ≠ []⟧
  ⟹ ∃a Q f. valid_edge a ∧ kind a = Q↩⇘get_proc n⇙f›
  from ‹n -as@[a]→* n'› have "n -as→* sourcenode a" and "valid_edge a"
    and "targetnode a = n'" by(auto intro:path_split_snoc)
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p"
    by(rule get_proc_return)
  with ‹kind a = Q↩⇘p⇙f› ‹valid_return_list cs n'› ‹valid_edge a› ‹targetnode a = n'›
  have "valid_return_list (a#cs) (sourcenode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(case_tac cs') apply auto
    apply(erule_tac x="list" in allE)
    apply(erule_tac x="c" in allE)
    by(auto split:list.split simp:targetnodes_def)
  from ‹∀xs ys. as@[a] = xs@ys ⟶
    ¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []› ‹kind a = Q↩⇘p⇙f›
  have "∀xs ys. as = xs@ys ⟶
    ¬ same_level_path_rev_aux (a#cs) ys ∨ upd_rev_cs (a#cs) ys ≠ []"
    apply clarsimp apply(erule_tac x="xs" in allE)
    by auto
  from IH[OF ‹n -as→* sourcenode a› ‹valid_return_list (a#cs) (sourcenode a)›
    _ this] show ?case by simp
next
  case (vpra_CallEmpty cs a as Q p fs)
  from ‹cs = []› ‹cs ≠ []› have False by simp
  thus ?case by simp
next
  case (vpra_CallCons cs a as Q r p fs c' cs')
  note IH = ‹⋀n'. ⟦n -as→* n'; valid_return_list cs' n'; cs' ≠ [];
    ∀xs ys. as = xs@ys ⟶
       ¬ same_level_path_rev_aux cs' ys ∨ upd_rev_cs cs' ys ≠ []⟧
    ⟹ ∃a Q f. valid_edge a ∧ kind a = Q↩⇘get_proc n⇙f›
  note all = ‹∀xs ys. as@[a] = xs@ys ⟶
     ¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []›
  from ‹n -as@[a]→* n'› have "n -as→* sourcenode a" and "valid_edge a"
    and "targetnode a = n'" by(auto intro:path_split_snoc)
  from ‹valid_return_list cs n'› ‹cs = c'#cs'› have "valid_edge c'"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="[]" in allE)
    by auto
  show ?case
  proof(cases "cs' = []")
    case True
    with ‹cs = c'#cs'› ‹kind a = Q:r↪⇘p⇙fs› ‹c' ∈ get_return_edges a›
    have "same_level_path_rev_aux cs ([]@[a])"
      and "upd_rev_cs cs ([]@[a]) = []"
      by(simp only:same_level_path_rev_aux.simps upd_rev_cs.simps,clarsimp)+
    with all have False by(erule_tac x="as" in allE) fastforce
    thus ?thesis by simp
  next
    case False
    with ‹valid_return_list cs n'› ‹cs = c'#cs'›
    have "valid_return_list cs' (targetnode c')"
      apply(clarsimp simp:valid_return_list_def)
      apply(hypsubst_thin)
      apply(erule_tac x="c'#cs'" in allE)
      apply(auto simp:targetnodes_def)
       apply(case_tac cs') apply auto
      apply(case_tac list) apply(auto simp:targetnodes_def)
      done
    from ‹valid_edge a› ‹c' ∈ get_return_edges a›
    have "get_proc (sourcenode a) = get_proc (targetnode c')"
      by(rule get_proc_get_return_edge)
    with ‹valid_return_list cs' (targetnode c')›
    have "valid_return_list cs' (sourcenode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(hypsubst_thin)
    apply(erule_tac x="cs'" in allE)
    apply(erule_tac x="c" in allE)
    by(auto split:list.split)
    from all ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c'#cs'› ‹c' ∈ get_return_edges a›
    have "∀xs ys. as = xs@ys 
      ⟶ ¬ same_level_path_rev_aux cs' ys ∨ upd_rev_cs cs' ys ≠ []"
      apply clarsimp apply(erule_tac x="xs" in allE)
      by auto  
    from IH[OF ‹n -as→* sourcenode a› ‹valid_return_list cs' (sourcenode a)›
      False this] show ?thesis .
  qed
qed


lemma valid_Entry_path_cases:
  assumes "(_Entry_) -as→⇩√* n" and "as ≠ []"
  shows "(∃a' as'. as = as'@[a'] ∧ intra_kind(kind a')) ∨
         (∃a' as' Q r p fs. as = as'@[a'] ∧ kind a' = Q:r↪⇘p⇙fs) ∨
         (∃as' as'' n'. as = as'@as'' ∧ as'' ≠ [] ∧ n' -as''→⇘sl⇙* n)"
proof -
  from ‹as ≠ []› obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto
  thus ?thesis
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra with ‹as = as'@[a']› show ?thesis by simp
  next
    case Call with ‹as = as'@[a']› show ?thesis by simp
  next
    case (Return Q p f)
    from ‹(_Entry_) -as→⇩√* n› have "(_Entry_) -as→* n" and "valid_path_rev_aux [] as"
      by(auto intro:vp_to_vpra simp:vp_def valid_path_def)
    from ‹(_Entry_) -as→* n› ‹as = as'@[a']›
    have "(_Entry_) -as'→* sourcenode a'" and "valid_edge a'" 
      and "targetnode a' = n"
      by(auto intro:path_split_snoc)
    from ‹valid_path_rev_aux [] as› ‹as = as'@[a']› Return
    have "valid_path_rev_aux [a'] as'" by simp
    from ‹valid_edge a'› Return
    have "valid_return_list [a'] (sourcenode a')"
      apply(clarsimp simp:valid_return_list_def)
      apply(case_tac cs') 
      by(auto intro:get_proc_return[THEN sym])
    show ?thesis
    proof(cases "∀xs ys. as' = xs@ys ⟶ 
        (¬ same_level_path_rev_aux [a'] ys ∨ upd_rev_cs [a'] ys ≠ [])")
      case True
      with ‹valid_path_rev_aux [a'] as'› ‹(_Entry_) -as'→* sourcenode a'›
        ‹valid_return_list [a'] (sourcenode a')›
      obtain ax Qx fx where "valid_edge ax" and "kind ax = Qx↩⇘get_proc (_Entry_)⇙fx"
        by(fastforce dest!:vpra_no_slpra)
      hence False by(fastforce intro:Main_no_return_source simp:get_proc_Entry)
      thus ?thesis by simp
    next
      case False
      then obtain xs ys where "as' = xs@ys" and "same_level_path_rev_aux [a'] ys"
        and "upd_rev_cs [a'] ys = []" by auto
      with Return have "same_level_path_rev_aux [] (ys@[a'])"
        and "upd_rev_cs [] (ys@[a']) = []" by simp_all
      from ‹upd_rev_cs [a'] ys = []› have "ys ≠ []" by auto
      with ‹(_Entry_) -as'→* sourcenode a'› ‹as' = xs@ys›
      have "hd(sourcenodes ys) -ys→* sourcenode a'"
        by(cases ys)(auto dest:path_split_second simp:sourcenodes_def)
      with ‹targetnode a' = n› ‹valid_edge a'›
      have "hd(sourcenodes ys) -ys@[a']→* n"
        by(fastforce intro:path_Append path_edge)
      with ‹same_level_path_rev_aux [] (ys@[a'])› ‹upd_rev_cs [] (ys@[a']) = []›
      have "same_level_path (ys@[a'])"
        by(fastforce dest:slpra_to_slpa simp:same_level_path_def valid_return_list_def)
      with ‹hd(sourcenodes ys) -ys@[a']→* n› have "hd(sourcenodes ys) -ys@[a']→⇘sl⇙* n"
        by(simp add:slp_def)
      with ‹as = as'@[a']› ‹as' = xs@ys› Return
      have "∃as' as'' n'. as = as'@as'' ∧ as'' ≠ [] ∧ n' -as''→⇘sl⇙* n"
        by(rule_tac x="xs" in exI) auto
      thus ?thesis by simp
    qed
  qed
qed


lemma valid_Entry_path_ascending_path:
  assumes "(_Entry_) -as→⇩√* n"
  obtains as' where "(_Entry_) -as'→⇩√* n" 
  and "set(sourcenodes as') ⊆ set(sourcenodes as)"
  and "∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
proof(atomize_elim)
  from ‹(_Entry_) -as→⇩√* n›
  show "∃as'. (_Entry_) -as'→⇩√* n ∧ set(sourcenodes as') ⊆ set(sourcenodes as)∧
              (∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs))"
  proof(induct as arbitrary:n rule:length_induct)
    fix as n
    assume IH:"∀as''. length as'' < length as ⟶
      (∀n'. (_Entry_) -as''→⇩√* n' ⟶
       (∃as'. (_Entry_) -as'→⇩√* n' ∧ set (sourcenodes as') ⊆ set (sourcenodes as'') ∧
              (∀a'∈set as'. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs))))"
      and "(_Entry_) -as→⇩√* n"
    show "∃as'. (_Entry_) -as'→⇩√* n ∧ set(sourcenodes as') ⊆ set(sourcenodes as)∧
              (∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs))"
    proof(cases "as = []")
      case True
      with ‹(_Entry_) -as→⇩√* n› show ?thesis by(fastforce simp:sourcenodes_def vp_def)
    next
      case False
      with ‹(_Entry_) -as→⇩√* n›
      have "((∃a' as'. as = as'@[a'] ∧ intra_kind(kind a')) ∨
         (∃a' as' Q r p fs. as = as'@[a'] ∧ kind a' = Q:r↪⇘p⇙fs)) ∨
         (∃as' as'' n'. as = as'@as'' ∧ as'' ≠ [] ∧ n' -as''→⇘sl⇙* n)"
        by(fastforce dest!:valid_Entry_path_cases)
      thus ?thesis apply -
      proof(erule disjE)+
        assume "∃a' as'. as = as'@[a'] ∧ intra_kind(kind a')"
        then obtain a' as' where "as = as'@[a']" and "intra_kind(kind a')" by blast
        from ‹(_Entry_) -as→⇩√* n› ‹as = as'@[a']›
        have "(_Entry_) -as'→⇩√* sourcenode a'" and "valid_edge a'"
          and "targetnode a' = n"
          by(auto intro:vp_split_snoc)
        from ‹valid_edge a'› ‹intra_kind(kind a')›
        have "sourcenode a' -[a']→⇘sl⇙* targetnode a'"
          by(fastforce intro:path_edge intras_same_level_path simp:slp_def)
        from IH ‹(_Entry_) -as'→⇩√* sourcenode a'› ‹as = as'@[a']›
        obtain xs where "(_Entry_) -xs→⇩√* sourcenode a'" 
          and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
          and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
          apply(erule_tac x="as'" in allE) by auto
        from ‹(_Entry_) -xs→⇩√* sourcenode a'› ‹sourcenode a' -[a']→⇘sl⇙* targetnode a'›
        have "(_Entry_) -xs@[a']→⇩√* targetnode a'" by(rule vp_slp_Append)
        with ‹targetnode a' = n› have "(_Entry_) -xs@[a']→⇩√* n" by simp
        moreover
        from ‹set (sourcenodes xs) ⊆ set (sourcenodes as')› ‹as = as'@[a']›
        have "set (sourcenodes (xs@[a'])) ⊆ set (sourcenodes as)"
          by(auto simp:sourcenodes_def)
        moreover
        from ‹∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)› 
          ‹intra_kind(kind a')›
        have "∀a'∈set (xs@[a']). intra_kind (kind a') ∨ 
                                 (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
          by fastforce
        ultimately show ?thesis by blast
      next
        assume "∃a' as' Q r p fs. as = as'@[a'] ∧ kind a' = Q:r↪⇘p⇙fs"
        then obtain a' as' Q r p fs where "as = as'@[a']" and "kind a' = Q:r↪⇘p⇙fs" 
          by blast
        from ‹(_Entry_) -as→⇩√* n› ‹as = as'@[a']›
        have "(_Entry_) -as'→⇩√* sourcenode a'" and "valid_edge a'"
          and "targetnode a' = n"
          by(auto intro:vp_split_snoc)
        from IH ‹(_Entry_) -as'→⇩√* sourcenode a'› ‹as = as'@[a']›
        obtain xs where "(_Entry_) -xs→⇩√* sourcenode a'" 
          and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
          and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
          apply(erule_tac x="as'" in allE) by auto
        from ‹targetnode a' = n› ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs›
          ‹(_Entry_) -xs→⇩√* sourcenode a'›
        have "(_Entry_) -xs@[a']→⇩√* n"
          by(fastforce intro:path_Append path_edge vpa_snoc_Call 
                       simp:vp_def valid_path_def)
        moreover
        from ‹set (sourcenodes xs) ⊆ set (sourcenodes as')› ‹as = as'@[a']›
        have "set (sourcenodes (xs@[a'])) ⊆ set (sourcenodes as)"
          by(auto simp:sourcenodes_def)
        moreover
        from ‹∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)› 
          ‹kind a' = Q:r↪⇘p⇙fs›
        have "∀a'∈set (xs@[a']). intra_kind (kind a') ∨ 
                                 (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
          by fastforce
        ultimately show ?thesis by blast
      next
        assume "∃as' as'' n'. as = as'@as'' ∧ as'' ≠ [] ∧ n' -as''→⇘sl⇙* n"
        then obtain as' as'' n' where "as = as'@as''" and "as'' ≠ []"
          and "n' -as''→⇘sl⇙* n" by blast
        from ‹(_Entry_) -as→⇩√* n› ‹as = as'@as''› ‹as'' ≠ []›
        have "(_Entry_) -as'→⇩√* hd(sourcenodes as'')"
          by(cases as'',auto intro:vp_split simp:sourcenodes_def)
        from ‹n' -as''→⇘sl⇙* n› ‹as'' ≠ []› have "hd(sourcenodes as'') = n'"
          by(fastforce intro:path_sourcenode simp:slp_def)
        from ‹as = as'@as''› ‹as'' ≠ []› have "length as' < length as" by simp
        with IH ‹(_Entry_) -as'→⇩√* hd(sourcenodes as'')›
          ‹hd(sourcenodes as'') = n'›
        obtain xs where "(_Entry_) -xs→⇩√* n'" 
          and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
          and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
          apply(erule_tac x="as'" in allE) by auto
        from ‹n' -as''→⇘sl⇙* n› obtain ys where "n' -ys→⇩ι* n"
          and "set(sourcenodes ys) ⊆ set(sourcenodes as'')"
          by(erule same_level_path_inner_path)
        from ‹(_Entry_) -xs→⇩√* n'› ‹n' -ys→⇩ι* n› have "(_Entry_) -xs@ys→⇩√* n"
          by(fastforce intro:vp_slp_Append intra_path_slp)
        moreover
        from ‹set (sourcenodes xs) ⊆ set (sourcenodes as')›
          ‹set(sourcenodes ys) ⊆ set(sourcenodes as'')› ‹as = as'@as''›
        have "set (sourcenodes (xs@ys)) ⊆ set(sourcenodes as)"
          by(auto simp:sourcenodes_def)
        moreover
        from ‹∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
          ‹n' -ys→⇩ι* n›
        have "∀a'∈set (xs@ys). intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
          by(fastforce simp:intra_path_def)
        ultimately show ?thesis by blast
      qed
    qed
  qed
qed



end

end